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 206  df-an 396

This theorem is referenced by:  syldanl  601  cases2ALT  1045  reximia  3172  2reu1  3826  difrab  4239  rabsnifsb  4655  foconst  6687  elfvmptrab  6885  dffo4  6961  dffo5  6962  isofrlem  7191  brfvopab  7310  onint  7617  el2mpocl  7897  suppofssd  7990  tz7.48lem  8242  opthreg  9306  eltsk2g  10438  recgt1i  11802  sup2  11861  elnnnn0c  12208  elnnz1  12276  recnz  12325  eluz2b2  12590  iccsplit  13146  elfzp12  13264  1mod  13551  pfxsuff1eqwrdeq  14340  cos01gt0  15828  oddnn02np1  15985  reumodprminv  16433  clatl  18141  isacs4lem  18177  isacs5lem  18178  isnzr2hash  20448  mplcoe5lem  21150  ioovolcl  24639  elply2  25262  cusgrsize  27724  rusgrpropedg  27854  wlkonprop  27928  wksonproplem  27974  pthdlem1  28035  3oalem1  29925  elorrvc  32330  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemodife  32364  ballotth  32404  nummin  32963  opnrebl2  34437  bj-eldiag2  35275  topdifinffinlem  35445  finxpsuc  35496  wl-ax11-lem3  35665  matunitlindflem2  35701  matunitlindf  35702  poimirlem28  35732  poimirlem29  35733  mblfinlem1  35741  ovoliunnfl  35746  voliunnfl  35748  itg2addnclem2  35756  areacirclem5  35796  seqpo  35832  incsequz  35833  incsequz2  35834  ismtycnv  35887  prnc  36152  dihatexv2  39280  isdomn4  40100  sn-sup2  40360  prjspval  40363  reabsifneg  41129  reabsifnpos  41130  reabsifpos  41131  reabsifnneg  41132  fperiodmullem  42732  climsuselem1  43038  climsuse  43039  0ellimcdiv  43080  fperdvper  43350  iblsplit  43397  stirlinglem11  43515  qndenserrnbllem  43725  sge0fodjrnlem  43844  upwlkbprop  45188  c0rnghm  45359  regt1loggt0  45770