Theorem imdistani 571

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syldanl  603  cases2ALT  1043  2reu1  3883  difrab  4279  rabsnifsb  4660  foconst  6605  elfvmptrab  6798  dffo4  6871  dffo5  6872  isofrlem  7095  brfvopab  7213  onint  7512  el2mpocl  7783  suppofssd  7869  tz7.48lem  8079  opthreg  9083  eltsk2g  10175  recgt1i  11539  sup2  11599  elnnnn0c  11945  elnnz1  12011  recnz  12060  eluz2b2  12324  iccsplit  12874  elfzp12  12989  1mod  13274  pfxsuff1eqwrdeq  14063  cos01gt0  15546  oddnn02np1  15699  reumodprminv  16143  clatl  17728  isacs4lem  17780  isacs5lem  17781  isnzr2hash  20039  mplcoe5lem  20250  ioovolcl  24173  elply2  24788  cusgrsize  27238  rusgrpropedg  27368  wlkonprop  27442  wksonproplem  27488  pthdlem1  27549  3oalem1  29441  elorrvc  31723  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemodife  31757  ballotth  31797  opnrebl2  33671  bj-eldiag2  34471  topdifinffinlem  34630  finxpsuc  34681  wl-ax11-lem3  34821  matunitlindflem2  34891  matunitlindf  34892  poimirlem28  34922  poimirlem29  34923  mblfinlem1  34931  ovoliunnfl  34936  voliunnfl  34938  itg2addnclem2  34946  areacirclem5  34988  seqpo  35024  incsequz  35025  incsequz2  35026  ismtycnv  35082  prnc  35347  dihatexv2  38477  prjspval  39260  fperiodmullem  41577  climsuselem1  41895  climsuse  41896  0ellimcdiv  41937  fperdvper  42210  iblsplit  42258  stirlinglem11  42376  qndenserrnbllem  42586  sge0fodjrnlem  42705  upwlkbprop  44020  c0rnghm  44191  regt1loggt0  44603