Theorem imdistani 572

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 559	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 410	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syldanl  605  cases2ALT  1048  2reu1  3786  difrab  4195  rabsnifsb  4610  foconst  6599  elfvmptrab  6797  dffo4  6873  dffo5  6874  isofrlem  7100  brfvopab  7219  onint  7523  el2mpocl  7800  suppofssd  7891  tz7.48lem  8099  opthreg  9147  eltsk2g  10244  recgt1i  11608  sup2  11667  elnnnn0c  12014  elnnz1  12082  recnz  12131  eluz2b2  12396  iccsplit  12952  elfzp12  13070  1mod  13355  pfxsuff1eqwrdeq  14143  cos01gt0  15629  oddnn02np1  15786  reumodprminv  16234  clatl  17835  isacs4lem  17887  isacs5lem  17888  isnzr2hash  20149  mplcoe5lem  20843  ioovolcl  24315  elply2  24937  cusgrsize  27388  rusgrpropedg  27518  wlkonprop  27592  wksonproplem  27638  pthdlem1  27699  3oalem1  29589  elorrvc  31992  ballotlemfc0  32021  ballotlemfcc  32022  ballotlemodife  32026  ballotth  32066  nummin  32626  opnrebl2  34140  bj-eldiag2  34958  topdifinffinlem  35130  finxpsuc  35181  wl-ax11-lem3  35350  matunitlindflem2  35386  matunitlindf  35387  poimirlem28  35417  poimirlem29  35418  mblfinlem1  35426  ovoliunnfl  35431  voliunnfl  35433  itg2addnclem2  35441  areacirclem5  35481  seqpo  35517  incsequz  35518  incsequz2  35519  ismtycnv  35572  prnc  35837  dihatexv2  38965  isdomn4  39748  sn-sup2  40000  prjspval  40003  reabsifneg  40769  reabsifnpos  40770  reabsifpos  40771  reabsifnneg  40772  fperiodmullem  42364  climsuselem1  42674  climsuse  42675  0ellimcdiv  42716  fperdvper  42986  iblsplit  43033  stirlinglem11  43151  qndenserrnbllem  43361  sge0fodjrnlem  43480  upwlkbprop  44818  c0rnghm  44989  regt1loggt0  45400