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  8458  add4  8487  2addsub  8540  addsubeq4  8541  sub4  8571  muladd  8711  mulsub  8728  add20i  8820  mulge0i  8948  mulap0b  8983  divmuldivap  9042  ltmul12a  9190  zmulcl  9698  uz2mulcl  10008  qaddcl  10035  qmulcl  10037  qreccl  10042  rpaddcl  10078  ge0addcl  10383  ge0xaddcl  10385  expge1  11013  rexanuz  11754  amgm2  11884  iooinsup  12043  mulcn2  12078  dvds2ln  12591  opoe  12662  omoe  12663  opeo  12664  omeo  12665  lcmgcd  12856  lcmdvds  12857  pc2dvds  13109  tgcl  15165  innei  15264  txbas  15359  txss12  15367  txbasval  15368  blsscls2  15594  qtopbasss  15622  lgslem3  16121  bj-indind  16958