Theorem imdistani 419

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  xoranor  1268  nfan1  1456  sbcof2  1691  difin  3174  difrab  3211  opthreg  4280  wessep  4302  fvelimab  5229  dffo4  5315  dffo5  5316  ltaddpr  6695  recgt1i  7864  elnnnn0c  8227  elnnz1  8268  recnz  8333  eluz2b2  8540  elfzp12  8961