Theorem an4s 508

Description: Inference rearranging 4 conjuncts in antecedent.

Hypothesis

Ref	Expression
an4s.1	|- (((ph /\ ps) /\ (ch /\ th)) -> ta)

Assertion

Ref	Expression
an4s	|- (((ph /\ ch) /\ (ps /\ th)) -> ta)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 506	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> ((ph /\ ps) /\ (ch /\ th)))
2		an4s.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
3	1, 2	sylbi 199	1 |- (((ph /\ ch) /\ (ps /\ th)) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anandis 512  anandirs 513  2mo 1447  fnun 3594  f1co 3667  f1oun 3706  f1oco 3707  tfrlem2 3912  tfrlem5 3915  brecop 4306  th3qlem1 4314  oprec 4318  undom 4438  mulclpi 5021  addcmpblnq 5052  mulcmpblnq 5053  mulpipq 5055  ordpipq 5056  mulclpq 5060  mulasspq 5065  distrpqlem 5066  distrpq 5067  ltapq 5076  genpnnp 5108  genpcd 5109  genpnmax 5110  prlem934 5139  addcmpblnr 5181  mulcmpblnr 5183  addsrpr 5184  mulsrpr 5185  ltsrpr 5186  addclsr 5192  mulclsr 5193  addasssr 5197  mulasssr 5199  distrsr 5200  mulgt0sr 5214  addresr 5256  mulresr 5257  axaddopr 5265  axmulopr 5266  axaddass 5277  axmulass 5278  axdistr 5279  add4t 5338  2addsubt 5389  mul4t 5420  muladdt 5421  addsub4t 5473  sub4t 5476  mulsubt 5477  muln0t 5698  divmuldivt 5780  divdivdivt 5785  recdivt 5790  ltmul12it 5841  lemul12itOLD 5843  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  nnleltp1t 5954  zaddclt 6165  zmulclt 6180  zltp1let 6181  qaddclt 6269  qmulclt 6271  rpaddclt 6290  rpmulclt 6291  ser1add2 6338  ser1add 6339  iooint 6372  sq11t 6629  creur 6742  creui 6743  climge0 7112  climmullem8 7127  iserzgt0 7211  reeff1o 7426  tgclt 7624  innei 7736  islp2 7747  metxp 7834  opnin 7869  iscms2lem3 7991  lmcau 7996  ajmoi 8519  ubthlem12 8540  ubthlem13 8541  spwmo 8656  hvadd4t 8905  hvsub4t 8906  hlimcaui 9106  pjtheu 9235  shsel3t 9279  shscl 9281  shscomt 9283  chj4t 9458  osumlem2 9579  5oalem3 9601  5oalem5 9603  5oalem6 9604  hoadd4t 9710  adjmo 9758  adjsymt 9759  cnvadj 9816  bra11 10041  hmopidmch 10079  mdslmd1lem2 10253  irredlem2 10318  irred 10321  cdjreu 10359  uninqs 10441  infi1 10447  infi1OLD 10448  filintf 10569  fgsb 10570  fgsbOLD 10571  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain