Theorem imdistani 449

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  453  xoranor  1426  nfan1  1617  sbcof2  1863  difin  3468  difrab  3507  rabsnifsb  3773  opthreg  4698  wessep  4720  fvelimab  5753  elfvmptrab  5795  dffo4  5847  dffo5  5848  ltaddpr  7954  recgt1i  9218  elnnnn0c  9587  elnnz1  9646  recnz  9718  eluz2b2  9982  elfzp12  10484  pfxsuff1eqwrdeq  11449  cos01gt0  12508  oddnn02np1  12625  reumodprminv  13010  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemth  13259  sgrpidmndm  13710  elply2  15759  bj-charfundc  16748