Theorem an42s 567

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  nnmsucr 5295  nnmsucrOLD 5296  ecopopreq 5367  sbthlem9 5518  addcmpblnq 6204  addpipq 6206  mulpipq 6207  addclpq 6210  addasspq 6215  distrpq 6219  recmulpq 6222  ltsopq 6227  ltexpq 6232  mulcmpblnr 6335  addsrpr 6336  mulsrpr 6337  mulclsr 6345  mulasssr 6351  distrsr 6352  ltsosr 6355  axmulopr 6418  axmulass 6431  axdistr 6432  subadd4 6642  mulsub 6644  tgcl 8894  hosubadd4 11377  difxp 15690  fdc 15812  isdivrng2 16111  unichnidl 16179

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 164  df-an 242

Copyright terms: Public domain