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  3099  2reu1  3848  difrab  4267  rabsnifsb  4686  foconst  6808  elfvmptrab  7020  dffo4  7100  dffo5  7101  isofrlem  7345  brfvopab  7474  onint  7793  el2mpocl  8087  suppofssd  8205  tz7.48lem  8434  opthreg  9601  eltsk2g  10764  recgt1i  12140  sup2  12199  elnnnn0c  12577  elnnz1  12648  recnz  12700  eluz2b2  12974  iccsplit  13542  elfzp12  13662  1mod  13968  pfxsuff1eqwrdeq  14772  cos01gt0  16285  oddnn02np1  16444  reumodprminv  16902  clatl  18602  isacs4lem  18638  isacs5lem  18639  isnzr2hash  20686  c0rnghm  20703  isdomn4  20883  mplcoe5lem  22261  matunitlindflem2  22908  matunitlindf  22909  ioovolcl  25804  elply2  26428  cusgrsize  29922  rusgrpropedg  30052  wlkonprop  30124  wksonproplem  30174  pthdlem1  30239  3oalem1  32151  elorrvc  34983  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemodife  35017  ballotth  35057  nummin  35606  opnrebl2  36948  bj-eldiag2  37937  topdifinffinlem  38109  finxpsuc  38160  poimirlem28  38405  poimirlem29  38406  mblfinlem1  38414  ovoliunnfl  38419  voliunnfl  38421  itg2addnclem2  38429  areacirclem5  38469  seqpo  38505  incsequz  38506  incsequz2  38507  ismtycnv  38560  prnc  38825  dihatexv2  42220  unitscyglem4  43072  sn-sup2  43387  prjspval  43457  tfsconcatlem  44185  omssrncard  44388  reabsifneg  44480  reabsifnpos  44481  reabsifpos  44482  reabsifnneg  44483  relpfrlem  45784  fperiodmullem  46144  climsuselem1  46445  climsuse  46446  0ellimcdiv  46485  fperdvper  46755  iblsplit  46802  stirlinglem11  46920  qndenserrnbllem  47130  sge0fodjrnlem  47252  upwlkbprop  49062  regt1loggt0  49474