Theorem an4s 590

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 586	. 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 )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an42s  591  anandis  594  anandirs  595  trin2  5120  fnun  5429  2elresin  5434  f1co  5545  f1oun  5594  f1oco  5597  f1mpt  5901  poxp  6384  tfrlem7  6469  brecop  6780  th3qlem1  6792  oviec  6796  pmss12g  6830  addcmpblnq  7565  mulcmpblnq  7566  mulpipqqs  7571  mulclnq  7574  mulcanenq  7583  distrnqg  7585  mulcmpblnq0  7642  mulcanenq0ec  7643  mulclnq0  7650  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  genipv  7707  genpelvl  7710  genpelvu  7711  genpml  7715  genpmu  7716  genpcdl  7717  genpcuu  7718  genprndl  7719  genprndu  7720  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  addcmpblnr  7937  ltsrprg  7945  addclsr  7951  mulclsr  7952  addasssrg  7954  addresr  8035  mulresr  8036  axaddass  8070  axmulass  8071  axdistr  8072  mulgt0  8232  mul4  8289  add4  8318  2addsub  8371  addsubeq4  8372  sub4  8402  muladd  8541  mulsub  8558  add20i  8650  mulge0i  8778  mulap0b  8813  divmuldivap  8870  ltmul12a  9018  zmulcl  9511  uz2mulcl  9815  qaddcl  9842  qmulcl  9844  qreccl  9849  rpaddcl  9885  ge0addcl  10189  ge0xaddcl  10191  expge1  10810  rexanuz  11515  amgm2  11645  iooinsup  11804  mulcn2  11839  dvds2ln  12351  opoe  12422  omoe  12423  opeo  12424  omeo  12425  lcmgcd  12616  lcmdvds  12617  pc2dvds  12869  tgcl  14754  innei  14853  txbas  14948  txss12  14956  txbasval  14957  blsscls2  15183  qtopbasss  15211  lgslem3  15697  bj-indind  16378