Theorem imdistani 442

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 327	. 2 |- ( ph -> ( ps -> ( ph /\ ch ) ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  xoranor  1367  nfan1  1552  sbcof2  1798  difin  3359  difrab  3396  opthreg  4533  wessep  4555  fvelimab  5542  elfvmptrab  5581  dffo4  5633  dffo5  5634  ltaddpr  7538  recgt1i  8793  elnnnn0c  9159  elnnz1  9214  recnz  9284  eluz2b2  9541  elfzp12  10034  cos01gt0  11703  oddnn02np1  11817  reumodprminv  12185  bj-charfundc  13690