Theorem an42s 391

Description: Inference rearranging 4 conjuncts in antecedent.

Hypothesis

Ref	Expression
an41r3s.1	|- (((ph /\ ps) /\ (ch /\ th)) -> ta )

Assertion

Ref	Expression
an42s	|- (((ph /\ ch) /\ (th /\ ps)) -> ta )

Proof of Theorem an42s

Step	Hyp	Ref	Expression
1		an42 389	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
2		an41r3s.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta )
3	1, 2	sylbir 176	1 |- (((ph /\ ch) /\ (th /\ ps)) -> ta )

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  f1oco 2816  nnmsucr 3182  ecopopreq 3244  sbthlem9 3357  addcmpblnq 3846  addpipq 3848  mulpipq 3849  addclpq 3852  addasspq 3857  distrpq 3861  recmulpq 3864  ltsopq 3869  ltexpq 3874  mulcmpblnr 3977  addsrpr 3978  mulsrpr 3979  mulclsr 3987  mulasssr 3993  distrsr 3994  ltsosr 3997  axmulcl 4068  axmulass 4073  axdistr 4074

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org