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  1396  nfan1  1586  sbcof2  1832  difin  3409  difrab  3446  opthreg  4603  wessep  4625  fvelimab  5634  elfvmptrab  5674  dffo4  5727  dffo5  5728  ltaddpr  7709  recgt1i  8970  elnnnn0c  9339  elnnz1  9394  recnz  9465  eluz2b2  9723  elfzp12  10220  cos01gt0  12045  oddnn02np1  12162  reumodprminv  12547  sgrpidmndm  13223  elply2  15178  bj-charfundc  15706