Theorem an4s 553

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

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 551	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
2		an4s.1	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
3	1, 2	sylbi 119	1 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) -> ta )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an42s  554  anandis  557  anandirs  558  trin2  4746  fnun  5036  2elresin  5041  f1co  5132  f1oun  5177  f1oco  5180  f1mpt  5442  poxp  5884  tfrlem7  5966  brecop  6262  th3qlem1  6274  oviec  6278  addcmpblnq  6619  mulcmpblnq  6620  mulpipqqs  6625  mulclnq  6628  mulcanenq  6637  distrnqg  6639  mulcmpblnq0  6696  mulcanenq0ec  6697  mulclnq0  6704  nqnq0a  6706  nqnq0m  6707  distrnq0  6711  genipv  6761  genpelvl  6764  genpelvu  6765  genpml  6769  genpmu  6770  genpcdl  6771  genpcuu  6772  genprndl  6773  genprndu  6774  distrlem1prl  6834  distrlem1pru  6835  ltsopr  6848  addcmpblnr  6978  ltsrprg  6986  addclsr  6992  mulclsr  6993  addasssrg  6995  addresr  7067  mulresr  7068  axaddass  7100  axmulass  7101  axdistr  7102  mulgt0  7253  mul4  7307  add4  7336  2addsub  7389  addsubeq4  7390  sub4  7420  muladd  7555  mulsub  7572  add20i  7660  mulge0i  7787  mulap0b  7812  divmuldivap  7867  ltmul12a  8005  zmulcl  8485  uz2mulcl  8776  qaddcl  8801  qmulcl  8803  qreccl  8808  rpaddcl  8838  ge0addcl  9080  serige0  9570  expge1  9610  rexanuz  10012  amgm2  10142  mulcn2  10289  dvds2ln  10373  opoe  10439  omoe  10440  opeo  10441  omeo  10442  lcmgcd  10604  lcmdvds  10605  bj-indind  10885