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  1366  nfan1  1551  sbcof2  1797  difin  3354  difrab  3391  opthreg  4527  wessep  4549  fvelimab  5536  elfvmptrab  5575  dffo4  5627  dffo5  5628  ltaddpr  7529  recgt1i  8784  elnnnn0c  9150  elnnz1  9205  recnz  9275  eluz2b2  9532  elfzp12  10024  cos01gt0  11689  oddnn02np1  11802  reumodprminv  12162  bj-charfundc  13525