HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem an42s 508
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
StepHypRef Expression
1 an42 506 . 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
2 an41r3s.1 . 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
31, 2sylbir 201 1 |- (((ph /\ ch) /\ (th /\ ps)) -> ta)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  nnmsucr 4224  ecopopreq 4292  sbthlem9 4435  addcmpblnq 5024  addpipq 5026  mulpipq 5027  addclpq 5030  addasspq 5035  distrpq 5039  recmulpq 5042  ltsopq 5047  ltexpq 5052  mulcmpblnr 5155  addsrpr 5156  mulsrpr 5157  mulclsr 5165  mulasssr 5171  distrsr 5172  ltsosr 5175  axmulopr 5238  axmulass 5250  axdistr 5251  subadd4t 5447  mulsubt 5449  tgclt 7566  hosubadd4t 9657
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