HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ancomsd 448
Description: Deduction commuting conjunction in antecedent.
Hypothesis
Ref Expression
ancomsd.1 |- (ph -> ((ps /\ ch) -> th))
Assertion
Ref Expression
ancomsd |- (ph -> ((ch /\ ps) -> th))

Proof of Theorem ancomsd
StepHypRef Expression
1 ancomsd.1 . 2 |- (ph -> ((ps /\ ch) -> th))
2 ancom 446 . 2 |- ((ch /\ ps) <-> (ps /\ ch))
31, 2syl5ib 213 1 |- (ph -> ((ch /\ ps) -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 230
This theorem is referenced by:  sylan2d 469  anabsi6 507  wereu 3002  cfub 4973  leltadd 5711  lemul12b 5900  lemul12aOLD 5901  iooss2 6399  znnenlem 7593  subgabl 8207  cvcon3 10295  atexch 10392  hmphtr 10625  hmeogrp 10632
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 154  df-an 232
Copyright terms: Public domain