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  1588  sbcof2  1834  difin  3418  difrab  3455  opthreg  4622  wessep  4644  fvelimab  5658  elfvmptrab  5698  dffo4  5751  dffo5  5752  ltaddpr  7745  recgt1i  9006  elnnnn0c  9375  elnnz1  9430  recnz  9501  eluz2b2  9759  elfzp12  10256  pfxsuff1eqwrdeq  11190  cos01gt0  12189  oddnn02np1  12306  reumodprminv  12691  sgrpidmndm  13367  elply2  15322  bj-charfundc  15943