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  1388  nfan1  1575  sbcof2  1821  difin  3397  difrab  3434  opthreg  4589  wessep  4611  fvelimab  5614  elfvmptrab  5654  dffo4  5707  dffo5  5708  ltaddpr  7659  recgt1i  8919  elnnnn0c  9288  elnnz1  9343  recnz  9413  eluz2b2  9671  elfzp12  10168  cos01gt0  11909  oddnn02np1  12024  reumodprminv  12394  sgrpidmndm  13004  elply2  14914  bj-charfundc  15370