Theorem imdistani 726

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  syldanl  735  cases2  993  nfan1OLD  2236  difrab  3901  rabsnifsb  4257  foconst  6126  elfvmptrab  6306  dffo4  6375  dffo5  6376  isofrlem  6590  brfvopab  6700  onint  6995  el2mpt2cl  7251  tz7.48lem  7536  opthreg  8515  eltsk2g  9573  recgt1i  10920  sup2  10979  elnnnn0c  11338  elnnz1  11403  recnz  11452  eluz2b2  11761  iccsplit  12305  elfzp12  12419  1mod  12702  2swrd1eqwrdeq  13454  cos01gt0  14921  oddnn02np1  15072  reumodprminv  15509  clatl  17116  isacs4lem  17168  isacs5lem  17169  isnzr2hash  19264  mplcoe5lem  19467  ioovolcl  23338  elply2  23952  cusgrsize  26350  rusgrpropedg  26480  wlkonprop  26554  wksonproplem  26601  pthdlem1  26662  numclwwlkovf2exlem2  27212  3oalem1  28521  elorrvc  30525  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  ballotth  30599  opnrebl2  32316  bj-eldiag2  33092  topdifinffinlem  33195  finxpsuc  33235  wl-ax11-lem3  33364  matunitlindflem2  33406  matunitlindf  33407  poimirlem28  33437  poimirlem29  33438  mblfinlem1  33446  ovoliunnfl  33451  voliunnfl  33453  itg2addnclem2  33462  areacirclem5  33504  seqpo  33543  incsequz  33544  incsequz2  33545  ismtycnv  33601  prnc  33866  dihatexv2  36628  fperiodmullem  39517  climsuselem1  39839  climsuse  39840  0ellimcdiv  39881  fperdvper  40133  iblsplit  40182  stirlinglem11  40301  qndenserrnbllem  40514  sge0fodjrnlem  40633  2reu1  41186  pfxsuff1eqwrdeq  41407  upwlkbprop  41719  c0rnghm  41913  regt1loggt0  42330