Theorem 3com13 838

Description: Commutation in antecedent. Swap 1st and 3rd.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3com13	|- ((ch /\ ps /\ ph) -> th)

Proof of Theorem 3com13

Step	Hyp	Ref	Expression
1		3anrev 784	. 2 |- ((ch /\ ps /\ ph) <-> (ph /\ ps /\ ch))
2		3exp.1	. 2 |- ((ph /\ ps /\ ch) -> th)
3	1, 2	sylbi 199	1 |- ((ch /\ ps /\ ph) -> th)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3coml 840  3adant3l 856  3adant3r 857  syld3an1 871  oacan 4182  oaword1 4186  ltapr 5151  ltaddsubt 5631  leaddsubt 5633  elfz2nn0t 6495  caure 6927  cauim 6928  faclbnd4 6952  2climnn 7102  2climnn0 7103  climsqueeze2 7141  caucvglem5 7161  infpnlem1 7506  ring2 8149  nvs 8290  ipdi 8503  ipsubdi 8509  spansncol 9491  irredlem2 10318  mdsymlem3 10332

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  df-3an 777

Copyright terms: Public domain