Theorem imdistani 579

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syldanl  614  cases2ALT  1064  reximia  3098  2reu1  3845  difrab  4264  rabsnifsb  4683  foconst  6803  elfvmptrab  7015  dffo4  7095  dffo5  7096  isofrlem  7340  brfvopab  7469  onint  7793  el2mpocl  8086  suppofssd  8204  tz7.48lemOLD  8435  opthreg  9603  eltsk2g  10817  recgt1i  12195  sup2  12254  elnnnn0c  12632  elnnz1  12703  recnz  12755  eluz2b2  13029  iccsplit  13597  elfzp12  13717  1mod  14023  pfxsuff1eqwrdeq  14828  cos01gt0  16339  oddnn02np1  16498  reumodprminv  16962  clatl  18662  isacs4lem  18698  isacs5lem  18699  isnzr2hash  20750  c0rnghm  20767  isdomn4  20947  mplcoe5lem  22328  matunitlindflem2  22975  matunitlindf  22976  ioovolcl  25871  elply2  26494  cusgrsize  30017  rusgrpropedg  30147  wlkonprop  30219  wksonproplem  30269  pthdlem1  30334  3oalem1  32246  elorrvc  35079  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemodife  35113  ballotth  35153  nummin  35701  opnrebl2  37079  bj-eldiag2  38066  topdifinffinlem  38238  finxpsuc  38289  poimirlem28  38534  poimirlem29  38535  mblfinlem1  38543  ovoliunnfl  38548  voliunnfl  38550  itg2addnclem2  38558  areacirclem5  38598  seqpo  38649  incsequz  38650  incsequz2  38651  ismtycnv  38704  prnc  38969  dihatexv2  42364  unitscyglem4  43216  sn-sup2  43523  prjspval  43593  tfsconcatlem  44296  omssrncard  44499  reabsifneg  44591  reabsifnpos  44592  reabsifpos  44593  reabsifnneg  44594  relpfrlem  45895  fperiodmullem  46262  climsuselem1  46563  climsuse  46564  0ellimcdiv  46603  fperdvper  46873  iblsplit  46920  stirlinglem11  47038  qndenserrnbllem  47248  sge0fodjrnlem  47370  upwlkbprop  49180  regt1loggt0  49592