Theorem imdistani 433

Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
imdistani.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
imdistani	|- ( ( ph /\ ps ) -> ( ph /\ ch ) )

Proof of Theorem imdistani

Step	Hyp	Ref	Expression
1		imdistani.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	anc2li 322	. 2 |- ( ph -> ( ps -> ( ph /\ ch ) ) )
3	2	imp 122	1 |- ( ( ph /\ ps ) -> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  xoranor  1308  nfan1  1496  sbcof2  1731  difin  3201  difrab  3238  opthreg  4299  wessep  4320  fvelimab  5250  dffo4  5336  dffo5  5337  ltaddpr  6787  recgt1i  7976  elnnnn0c  8333  elnnz1  8374  recnz  8440  eluz2b2  8690  elfzp12  9116  oddnn02np1  10280