Theorem imdistani 722

Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
imdistani.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imdistani	⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Proof of Theorem imdistani

Step	Hyp	Ref	Expression
1		imdistani.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	anc2li 578	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 444	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  syldanl  731  cases2  1005  nfan1OLD  2224  difrab  3860  rabsnifsb  4201  foconst  6039  elfvmptrab  6214  dffo4  6283  dffo5  6284  isofrlem  6490  brfvopab  6598  onint  6887  el2mpt2cl  7138  tz7.48lem  7423  opthreg  8398  eltsk2g  9452  recgt1i  10799  sup2  10858  elnnnn0c  11215  elnnz1  11280  recnz  11328  eluz2b2  11637  iccsplit  12176  elfzp12  12288  1mod  12564  2swrd1eqwrdeq  13306  cos01gt0  14760  oddnn02np1  14910  reumodprminv  15347  clatl  16939  isacs4lem  16991  isacs5lem  16992  isnzr2hash  19085  mplcoe5lem  19288  ioovolcl  23144  elply2  23756  wlkonprop  26063  trlonprop  26072  pthonprop  26107  spthonprp  26115  3oalem1  27905  elorrvc  29852  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemodife  29886  ballotth  29926  opnrebl2  31486  bj-eldiag2  32269  topdifinffinlem  32371  finxpsuc  32411  wl-ax11-lem3  32543  matunitlindflem2  32576  matunitlindf  32577  poimirlem28  32607  poimirlem29  32608  mblfinlem1  32616  ovoliunnfl  32621  voliunnfl  32623  itg2addnclem2  32632  areacirclem5  32674  seqpo  32713  incsequz  32714  incsequz2  32715  ismtycnv  32771  prnc  33036  dihatexv2  35646  fperiodmullem  38458  climsuselem1  38674  climsuse  38675  0ellimcdiv  38716  fperdvper  38808  iblsplit  38858  stirlinglem11  38977  qndenserrnbllem  39190  sge0fodjrnlem  39309  2reu1  39835  pfxsuff1eqwrdeq  40270  cusgrsize  40670  rusgrpropedg  40784  wlkbProp  40817  wlkOnprop  40866  1wlksonproplem  40912  pthdlem1  40972  c0rnghm  41703  regt1loggt0  42128