Theorem imdistani 576

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  syldanl  611  cases2ALT  1059  reximia  3096  2reu1  3848  difrab  4268  rabsnifsb  4678  foconst  6787  elfvmptrab  6999  dffo4  7078  dffo5  7079  isofrlem  7318  brfvopab  7447  onint  7767  el2mpocl  8058  suppofssd  8176  tz7.48lem  8405  opthreg  9566  eltsk2g  10702  recgt1i  12082  sup2  12141  elnnnn0c  12519  elnnz1  12590  recnz  12641  eluz2b2  12915  iccsplit  13482  elfzp12  13601  1mod  13906  pfxsuff1eqwrdeq  14705  cos01gt0  16213  oddnn02np1  16372  reumodprminv  16830  clatl  18530  isacs4lem  18566  isacs5lem  18567  isnzr2hash  20555  c0rnghm  20571  isdomn4  20752  mplcoe5lem  22079  ioovolcl  25619  elply2  26243  cusgrsize  29611  rusgrpropedg  29741  wlkonprop  29813  wksonproplem  29859  pthdlem1  29922  3oalem1  31821  elorrvc  34721  ballotlemfc0  34750  ballotlemfcc  34751  ballotlemodife  34755  ballotth  34795  nummin  35349  opnrebl2  36641  bj-eldiag2  37629  topdifinffinlem  37801  finxpsuc  37852  matunitlindflem2  38076  matunitlindf  38077  poimirlem28  38107  poimirlem29  38108  mblfinlem1  38116  ovoliunnfl  38121  voliunnfl  38123  itg2addnclem2  38131  areacirclem5  38171  seqpo  38206  incsequz  38207  incsequz2  38208  ismtycnv  38261  prnc  38526  dihatexv2  41923  unitscyglem4  42775  sn-sup2  43073  prjspval  43145  tfsconcatlem  43873  omssrncard  44076  reabsifneg  44168  reabsifnpos  44169  reabsifpos  44170  reabsifnneg  44171  relpfrlem  45489  fperiodmullem  45842  climsuselem1  46143  climsuse  46144  0ellimcdiv  46183  fperdvper  46453  iblsplit  46500  stirlinglem11  46618  qndenserrnbllem  46828  sge0fodjrnlem  46950  upwlkbprop  48720  regt1loggt0  49118