Theorem imdistani 437

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 325	. 2 |- ( ph -> ( ps -> ( ph /\ ch ) ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  xoranor  1323  nfan1  1511  sbcof2  1749  difin  3260  difrab  3297  opthreg  4409  wessep  4430  fvelimab  5409  elfvmptrab  5448  dffo4  5500  dffo5  5501  ltaddpr  7306  recgt1i  8514  elnnnn0c  8874  elnnz1  8929  recnz  8996  eluz2b2  9247  elfzp12  9720  cos01gt0  11267  oddnn02np1  11372