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  1397  nfan1  1587  sbcof2  1833  difin  3410  difrab  3447  opthreg  4604  wessep  4626  fvelimab  5635  elfvmptrab  5675  dffo4  5728  dffo5  5729  ltaddpr  7710  recgt1i  8971  elnnnn0c  9340  elnnz1  9395  recnz  9466  eluz2b2  9724  elfzp12  10221  cos01gt0  12074  oddnn02np1  12191  reumodprminv  12576  sgrpidmndm  13252  elply2  15207  bj-charfundc  15744