Theorem ancomsd 269

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

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		ancom 266	. 2 |- ( ( ch /\ ps ) <-> ( ps /\ ch ) )
2		ancomsd.1	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	1, 2	biimtrid 152	1 |- ( ph -> ( ( ch /\ ps ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylan2d  294  mpand  429  anabsi6  582  ralxfrd  4588  rexxfrd  4589  poirr2  5160  smoel  6544  genprndl  7852  genprndu  7853  addcanprlemu  7946  leltadd  8738  lemul12b  9152  lbzbi  9966  dvdssub2  12546  odzdvds  12968  wlk1walkdom  16480