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  3103  2reu1  3854  difrab  4274  rabsnifsb  4693  foconst  6814  elfvmptrab  7026  dffo4  7105  dffo5  7106  isofrlem  7349  brfvopab  7480  onint  7798  el2mpocl  8090  suppofssd  8208  tz7.48lem  8437  opthreg  9597  eltsk2g  10754  recgt1i  12130  sup2  12189  elnnnn0c  12567  elnnz1  12638  recnz  12689  eluz2b2  12963  iccsplit  13530  elfzp12  13650  1mod  13956  pfxsuff1eqwrdeq  14760  cos01gt0  16272  oddnn02np1  16431  reumodprminv  16889  clatl  18589  isacs4lem  18625  isacs5lem  18626  isnzr2hash  20654  c0rnghm  20671  isdomn4  20851  mplcoe5lem  22227  ioovolcl  25766  elply2  26390  cusgrsize  29841  rusgrpropedg  29971  wlkonprop  30043  wksonproplem  30089  pthdlem1  30152  3oalem1  32051  elorrvc  34886  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemodife  34920  ballotth  34960  nummin  35509  opnrebl2  36873  bj-eldiag2  37862  topdifinffinlem  38034  finxpsuc  38085  matunitlindflem2  38309  matunitlindf  38310  poimirlem28  38340  poimirlem29  38341  mblfinlem1  38349  ovoliunnfl  38354  voliunnfl  38356  itg2addnclem2  38364  areacirclem5  38404  seqpo  38439  incsequz  38440  incsequz2  38441  ismtycnv  38494  prnc  38759  dihatexv2  42154  unitscyglem4  43006  sn-sup2  43306  prjspval  43376  tfsconcatlem  44104  omssrncard  44307  reabsifneg  44399  reabsifnpos  44400  reabsifpos  44401  reabsifnneg  44402  relpfrlem  45703  fperiodmullem  46063  climsuselem1  46364  climsuse  46365  0ellimcdiv  46404  fperdvper  46674  iblsplit  46721  stirlinglem11  46839  qndenserrnbllem  47049  sge0fodjrnlem  47171  upwlkbprop  48944  regt1loggt0  49357