Theorem imdistani 568

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syldanl  601  cases2ALT  1049  reximia  3087  2reu1  3919  difrab  4337  rabsnifsb  4747  foconst  6849  elfvmptrab  7058  dffo4  7137  dffo5  7138  isofrlem  7376  brfvopab  7507  onint  7826  el2mpocl  8127  suppofssd  8244  tz7.48lem  8497  opthreg  9687  eltsk2g  10820  recgt1i  12192  sup2  12251  elnnnn0c  12598  elnnz1  12669  recnz  12718  eluz2b2  12986  iccsplit  13545  elfzp12  13663  1mod  13954  pfxsuff1eqwrdeq  14747  cos01gt0  16239  oddnn02np1  16396  reumodprminv  16851  clatl  18578  isacs4lem  18614  isacs5lem  18615  isnzr2hash  20545  c0rnghm  20561  isdomn4  20738  mplcoe5lem  22080  ioovolcl  25624  elply2  26255  cusgrsize  29490  rusgrpropedg  29620  wlkonprop  29694  wksonproplem  29740  wksonproplemOLD  29741  pthdlem1  29802  3oalem1  31694  elorrvc  34428  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotth  34502  nummin  35067  opnrebl2  36287  bj-eldiag2  37143  topdifinffinlem  37313  finxpsuc  37364  wl-ax11-lem3  37541  matunitlindflem2  37577  matunitlindf  37578  poimirlem28  37608  poimirlem29  37609  mblfinlem1  37617  ovoliunnfl  37622  voliunnfl  37624  itg2addnclem2  37632  areacirclem5  37672  seqpo  37707  incsequz  37708  incsequz2  37709  ismtycnv  37762  prnc  38027  dihatexv2  41296  unitscyglem4  42155  sn-sup2  42447  prjspval  42558  tfsconcatlem  43298  omssrncard  43502  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  fperiodmullem  45218  climsuselem1  45528  climsuse  45529  0ellimcdiv  45570  fperdvper  45840  iblsplit  45887  stirlinglem11  46005  qndenserrnbllem  46215  sge0fodjrnlem  46337  upwlkbprop  47861  regt1loggt0  48270