Theorem imdistani 569

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syldanl  602  cases2ALT  1046  reximia  3176  2reu1  3830  difrab  4242  rabsnifsb  4658  foconst  6703  elfvmptrab  6903  dffo4  6979  dffo5  6980  isofrlem  7211  brfvopab  7332  onint  7640  el2mpocl  7926  suppofssd  8019  tz7.48lem  8272  opthreg  9376  eltsk2g  10507  recgt1i  11872  sup2  11931  elnnnn0c  12278  elnnz1  12346  recnz  12395  eluz2b2  12661  iccsplit  13217  elfzp12  13335  1mod  13623  pfxsuff1eqwrdeq  14412  cos01gt0  15900  oddnn02np1  16057  reumodprminv  16505  clatl  18226  isacs4lem  18262  isacs5lem  18263  isnzr2hash  20535  mplcoe5lem  21240  ioovolcl  24734  elply2  25357  cusgrsize  27821  rusgrpropedg  27951  wlkonprop  28026  wksonproplem  28072  wksonproplemOLD  28073  pthdlem1  28134  3oalem1  30024  elorrvc  32430  ballotlemfc0  32459  ballotlemfcc  32460  ballotlemodife  32464  ballotth  32504  nummin  33063  opnrebl2  34510  bj-eldiag2  35348  topdifinffinlem  35518  finxpsuc  35569  wl-ax11-lem3  35738  matunitlindflem2  35774  matunitlindf  35775  poimirlem28  35805  poimirlem29  35806  mblfinlem1  35814  ovoliunnfl  35819  voliunnfl  35821  itg2addnclem2  35829  areacirclem5  35869  seqpo  35905  incsequz  35906  incsequz2  35907  ismtycnv  35960  prnc  36225  dihatexv2  39353  isdomn4  40172  sn-sup2  40439  prjspval  40442  omssrncard  41147  reabsifneg  41240  reabsifnpos  41241  reabsifpos  41242  reabsifnneg  41243  fperiodmullem  42842  climsuselem1  43148  climsuse  43149  0ellimcdiv  43190  fperdvper  43460  iblsplit  43507  stirlinglem11  43625  qndenserrnbllem  43835  sge0fodjrnlem  43954  upwlkbprop  45300  c0rnghm  45471  regt1loggt0  45882