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 1445  fnun 3586  f1co 3658  f1oun 3697  f1oco 3698  tfrlem2 3903  tfrlem5 3906  brecop 4296  th3qlem1 4304  oprec 4308  undom 4424  mulclpi 5001  addcmpblnq 5032  mulcmpblnq 5033  mulpipq 5035  ordpipq 5036  mulclpq 5040  mulasspq 5045  distrpqlem 5046  distrpq 5047  ltapq 5056  genpnnp 5088  genpcd 5089  genpnmax 5090  prlem934 5119  addcmpblnr 5161  mulcmpblnr 5163  addsrpr 5164  mulsrpr 5165  ltsrpr 5166  addclsr 5172  mulclsr 5173  addasssr 5177  mulasssr 5179  distrsr 5180  mulgt0sr 5194  addresr 5236  mulresr 5237  axaddopr 5245  axmulopr 5246  axaddass 5257  axmulass 5258  axdistr 5259  add4t 5318  2addsubt 5369  mul4t 5400  muladdt 5401  addsub4t 5453  sub4t 5456  mulsubt 5457  muln0t 5675  divmuldivt 5744  divdivdivt 5749  recdivt 5754  ltmul12it 5805  lemul12itOLD 5807  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  nnleltp1t 5909  zaddclt 6120  zmulclt 6135  zltp1let 6136  qaddclt 6215  qmulclt 6217  rpaddclt 6235  rpmulclt 6236  ser1add2 6283  ser1add 6284  iooint 6317  sq11t 6568  creur 6681  creui 6682  climge0 7057  climmullem8 7071  iserzgt0 7154  reeff1o 7376  tgclt 7574  innei 7686  islp2 7697  metxp 7786  opnin 7821  iscms2lem3 7941  lmcau 7946  ajmoi 8463  ubthlem12 8484  ubthlem13 8485  spwmo 8598  hvadd4t 8844  hvsub4t 8845  hlimcaui 9045  pjtheu 9173  shsel3t 9217  shscl 9219  shscomt 9221  chj4t 9396  osumlem2 9519  5oalem3 9541  5oalem5 9543  5oalem6 9544  hoadd4t 9650  adjmo 9698  adjsymt 9699  cnvadj 9756  bra11 9979  hmopidmch 10017  mdslmd1lem2 10190  irredlem2 10255  irred 10258  cdjreu 10293  uninqs 10378  infi1 10383  filintf 10479  fgsb 10480  fgsb2 10485

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