Theorem an42s 509

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 507	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
2		an41r3s.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
3	1, 2	sylbir 201	1 |- (((ph /\ ch) /\ (th /\ ps)) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  nnmsucr 4230  ecopopreq 4298  sbthlem9 4441  addcmpblnq 5032  addpipq 5034  mulpipq 5035  addclpq 5038  addasspq 5043  distrpq 5047  recmulpq 5050  ltsopq 5055  ltexpq 5060  mulcmpblnr 5163  addsrpr 5164  mulsrpr 5165  mulclsr 5173  mulasssr 5179  distrsr 5180  ltsosr 5183  axmulopr 5246  axmulass 5258  axdistr 5259  subadd4t 5455  mulsubt 5457  tgclt 7574  hosubadd4t 9680

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain