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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylan2d  294  mpand  433  anabsi6  586  ralxfrd  4610  rexxfrd  4611  poirr2  5183  smoel  6575  genprndl  7894  genprndu  7895  addcanprlemu  7988  leltadd  8782  lemul12b  9199  lbzbi  10032  dvdssub2  12627  odzdvds  13053  wlk1walkdom  16805