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  1377  nfan1  1564  sbcof2  1810  difin  3374  difrab  3411  opthreg  4557  wessep  4579  fvelimab  5575  elfvmptrab  5614  dffo4  5667  dffo5  5668  ltaddpr  7599  recgt1i  8858  elnnnn0c  9224  elnnz1  9279  recnz  9349  eluz2b2  9606  elfzp12  10102  cos01gt0  11773  oddnn02np1  11888  reumodprminv  12256  sgrpidmndm  12827  bj-charfundc  14700