Theorem imdistani 578

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  syldanl  613  cases2ALT  1062  reximia  3100  2reu1  3853  difrab  4273  rabsnifsb  4684  foconst  6797  elfvmptrab  7009  dffo4  7088  dffo5  7089  isofrlem  7328  brfvopab  7457  onint  7777  el2mpocl  8069  suppofssd  8187  tz7.48lem  8416  opthreg  9575  eltsk2g  10724  recgt1i  12100  sup2  12159  elnnnn0c  12537  elnnz1  12608  recnz  12659  eluz2b2  12933  iccsplit  13500  elfzp12  13619  1mod  13924  pfxsuff1eqwrdeq  14724  cos01gt0  16235  oddnn02np1  16394  reumodprminv  16852  clatl  18552  isacs4lem  18588  isacs5lem  18589  isnzr2hash  20591  c0rnghm  20608  isdomn4  20788  mplcoe5lem  22147  ioovolcl  25686  elply2  26310  cusgrsize  29709  rusgrpropedg  29839  wlkonprop  29911  wksonproplem  29957  pthdlem1  30020  3oalem1  31919  elorrvc  34766  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemodife  34800  ballotth  34840  nummin  35394  opnrebl2  36689  bj-eldiag2  37676  topdifinffinlem  37848  finxpsuc  37899  matunitlindflem2  38123  matunitlindf  38124  poimirlem28  38154  poimirlem29  38155  mblfinlem1  38163  ovoliunnfl  38168  voliunnfl  38170  itg2addnclem2  38178  areacirclem5  38218  seqpo  38253  incsequz  38254  incsequz2  38255  ismtycnv  38308  prnc  38573  dihatexv2  41970  unitscyglem4  42822  sn-sup2  43120  prjspval  43192  tfsconcatlem  43920  omssrncard  44123  reabsifneg  44215  reabsifnpos  44216  reabsifpos  44217  reabsifnneg  44218  relpfrlem  45521  fperiodmullem  45881  climsuselem1  46182  climsuse  46183  0ellimcdiv  46222  fperdvper  46492  iblsplit  46539  stirlinglem11  46657  qndenserrnbllem  46867  sge0fodjrnlem  46989  upwlkbprop  48759  regt1loggt0  49168