Theorem an42s 511

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 509	. 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 4246  ecopopreq 4314  sbthlem9 4461  addcmpblnq 5064  addpipq 5066  mulpipq 5067  addclpq 5070  addasspq 5075  distrpq 5079  recmulpq 5082  ltsopq 5087  ltexpq 5092  mulcmpblnr 5195  addsrpr 5196  mulsrpr 5197  mulclsr 5205  mulasssr 5211  distrsr 5212  ltsosr 5215  axmulopr 5278  axmulass 5290  axdistr 5291  subadd4t 5487  mulsubt 5489  tgclt 7623  hosubadd4t 9735

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