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

Step	Hyp	Ref	Expression
1		ancomsd.1	. 2 |- (ph -> ((ps /\ ch) -> th))
2		ancom 446	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
3	1, 2	syl5ib 213	1 |- (ph -> ((ch /\ ps) -> th))

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