Theorem ancomsd 437

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 435	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
3	1, 2	syl5ib 206	1 |- (ph -> ((ch /\ ps) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylan2d 458  anabsi6 496  wereu 2945  cfub 4908  leltaddt 5646  lemul12ait 5842  lemul12itOLD 5843  iooss2 6374  znnenlem 7501  subgabl 8123  cvcon3t 10211  atexcht 10308  hmphtr 10531  hmeogrp 10538

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