Theorem imdistani 445

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

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 is referenced by:  syldanl  449  xoranor  1422  nfan1  1613  sbcof2  1859  difin  3458  difrab  3495  rabsnifsb  3757  opthreg  4678  wessep  4700  fvelimab  5733  elfvmptrab  5773  dffo4  5825  dffo5  5826  ltaddpr  7912  recgt1i  9172  elnnnn0c  9541  elnnz1  9600  recnz  9671  eluz2b2  9935  elfzp12  10433  pfxsuff1eqwrdeq  11391  cos01gt0  12449  oddnn02np1  12566  reumodprminv  12951  sgrpidmndm  13633  elply2  15600  bj-charfundc  16578