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  1421  nfan1  1612  sbcof2  1858  difin  3444  difrab  3481  rabsnifsb  3737  opthreg  4654  wessep  4676  fvelimab  5702  elfvmptrab  5742  dffo4  5795  dffo5  5796  ltaddpr  7817  recgt1i  9078  elnnnn0c  9447  elnnz1  9502  recnz  9573  eluz2b2  9837  elfzp12  10334  pfxsuff1eqwrdeq  11284  cos01gt0  12342  oddnn02np1  12459  reumodprminv  12844  sgrpidmndm  13521  elply2  15478  bj-charfundc  16454