Theorem imdistani 573

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 560	. 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 208  df-an 397

This theorem is referenced by:  syldanl  608  cases2ALT  1054  reximia  3075  2reu1  3836  difrab  4253  rabsnifsb  4661  foconst  6761  elfvmptrab  6972  dffo4  7051  dffo5  7052  isofrlem  7291  brfvopab  7420  onint  7740  el2mpocl  8032  suppofssd  8150  tz7.48lem  8377  opthreg  9537  eltsk2g  10672  recgt1i  12051  sup2  12110  elnnnn0c  12480  elnnz1  12551  recnz  12602  eluz2b2  12869  iccsplit  13436  elfzp12  13555  1mod  13860  pfxsuff1eqwrdeq  14659  cos01gt0  16156  oddnn02np1  16315  reumodprminv  16773  clatl  18472  isacs4lem  18508  isacs5lem  18509  isnzr2hash  20498  c0rnghm  20514  isdomn4  20695  mplcoe5lem  22022  ioovolcl  25562  elply2  26186  cusgrsize  29548  rusgrpropedg  29678  wlkonprop  29750  wksonproplem  29796  pthdlem1  29859  3oalem1  31758  elorrvc  34655  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemodife  34689  ballotth  34729  nummin  35281  opnrebl2  36556  bj-eldiag2  37544  topdifinffinlem  37716  finxpsuc  37767  matunitlindflem2  37991  matunitlindf  37992  poimirlem28  38022  poimirlem29  38023  mblfinlem1  38031  ovoliunnfl  38036  voliunnfl  38038  itg2addnclem2  38046  areacirclem5  38086  seqpo  38121  incsequz  38122  incsequz2  38123  ismtycnv  38176  prnc  38441  dihatexv2  41838  unitscyglem4  42690  sn-sup2  42988  prjspval  43060  tfsconcatlem  43788  omssrncard  43991  reabsifneg  44083  reabsifnpos  44084  reabsifpos  44085  reabsifnneg  44086  relpfrlem  45404  fperiodmullem  45758  climsuselem1  46059  climsuse  46060  0ellimcdiv  46099  fperdvper  46369  iblsplit  46416  stirlinglem11  46534  qndenserrnbllem  46744  sge0fodjrnlem  46866  upwlkbprop  48636  regt1loggt0  49034