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  602  cases2ALT  1048  reximia  3071  2reu1  3872  difrab  4293  rabsnifsb  4698  foconst  6805  elfvmptrab  7015  dffo4  7093  dffo5  7094  isofrlem  7333  brfvopab  7464  onint  7784  el2mpocl  8085  suppofssd  8202  tz7.48lem  8455  opthreg  9632  eltsk2g  10765  recgt1i  12139  sup2  12198  elnnnn0c  12546  elnnz1  12618  recnz  12668  eluz2b2  12937  iccsplit  13502  elfzp12  13620  1mod  13920  pfxsuff1eqwrdeq  14717  cos01gt0  16209  oddnn02np1  16367  reumodprminv  16824  clatl  18518  isacs4lem  18554  isacs5lem  18555  isnzr2hash  20479  c0rnghm  20495  isdomn4  20676  mplcoe5lem  21997  ioovolcl  25523  elply2  26153  cusgrsize  29434  rusgrpropedg  29564  wlkonprop  29638  wksonproplem  29684  wksonproplemOLD  29685  pthdlem1  29748  3oalem1  31643  elorrvc  34496  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemodife  34530  ballotth  34570  nummin  35122  opnrebl2  36339  bj-eldiag2  37195  topdifinffinlem  37365  finxpsuc  37416  wl-ax11-lem3  37605  matunitlindflem2  37641  matunitlindf  37642  poimirlem28  37672  poimirlem29  37673  mblfinlem1  37681  ovoliunnfl  37686  voliunnfl  37688  itg2addnclem2  37696  areacirclem5  37736  seqpo  37771  incsequz  37772  incsequz2  37773  ismtycnv  37826  prnc  38091  dihatexv2  41358  unitscyglem4  42211  sn-sup2  42514  prjspval  42626  tfsconcatlem  43360  omssrncard  43564  reabsifneg  43656  reabsifnpos  43657  reabsifpos  43658  reabsifnneg  43659  relpfrlem  44978  fperiodmullem  45332  climsuselem1  45636  climsuse  45637  0ellimcdiv  45678  fperdvper  45948  iblsplit  45995  stirlinglem11  46113  qndenserrnbllem  46323  sge0fodjrnlem  46445  upwlkbprop  48113  regt1loggt0  48516