Theorem an4s 596

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42s  597  anandis  600  anandirs  601  trin2  5179  fnun  5489  2elresin  5494  f1co  5610  f1oun  5659  f1oco  5662  f1mpt  5977  poxp  6468  tfrlem7  6588  brecop  6899  th3qlem1  6911  oviec  6915  pmss12g  6956  addcmpblnq  7734  mulcmpblnq  7735  mulpipqqs  7740  mulclnq  7743  mulcanenq  7752  distrnqg  7754  mulcmpblnq0  7811  mulcanenq0ec  7812  mulclnq0  7819  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  genipv  7876  genpelvl  7879  genpelvu  7880  genpml  7884  genpmu  7885  genpcdl  7886  genpcuu  7887  genprndl  7888  genprndu  7889  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  addcmpblnr  8106  ltsrprg  8114  addclsr  8120  mulclsr  8121  addasssrg  8123  addresr  8204  mulresr  8205  axaddass  8239  axmulass  8240  axdistr  8241  mulgt0  8400  mul4  8459  add4  8488  2addsub  8541  addsubeq4  8542  sub4  8572  muladd  8712  mulsub  8729  add20i  8821  mulge0i  8950  mulap0b  8985  divmuldivap  9044  ltmul12a  9192  zmulcl  9702  uz2mulcl  10017  qaddcl  10044  qmulcl  10046  qreccl  10051  rpaddcl  10088  ge0addcl  10393  ge0xaddcl  10395  expge1  11026  rexanuz  11768  amgm2  11899  iooinsup  12059  mulcn2  12094  dvds2ln  12607  opoe  12678  omoe  12679  opeo  12680  omeo  12681  lcmgcd  12872  lcmdvds  12873  pc2dvds  13129  tgcl  15214  innei  15313  txbas  15408  txss12  15416  txbasval  15417  blsscls2  15643  qtopbasss  15671  lgslem3  16219  bj-indind  17056