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  1388  nfan1  1575  sbcof2  1821  difin  3396  difrab  3433  opthreg  4588  wessep  4610  fvelimab  5613  elfvmptrab  5653  dffo4  5706  dffo5  5707  ltaddpr  7657  recgt1i  8917  elnnnn0c  9285  elnnz1  9340  recnz  9410  eluz2b2  9668  elfzp12  10165  cos01gt0  11906  oddnn02np1  12021  reumodprminv  12391  sgrpidmndm  13001  elply2  14881  bj-charfundc  15300