Theorem imdistani 570

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  syldanl  603  cases2ALT  1048  reximia  3082  2reu1  3890  difrab  4307  rabsnifsb  4725  foconst  6817  elfvmptrab  7022  dffo4  7100  dffo5  7101  isofrlem  7332  brfvopab  7461  onint  7773  el2mpocl  8067  suppofssd  8183  tz7.48lem  8436  opthreg  9609  eltsk2g  10742  recgt1i  12107  sup2  12166  elnnnn0c  12513  elnnz1  12584  recnz  12633  eluz2b2  12901  iccsplit  13458  elfzp12  13576  1mod  13864  pfxsuff1eqwrdeq  14645  cos01gt0  16130  oddnn02np1  16287  reumodprminv  16733  clatl  18457  isacs4lem  18493  isacs5lem  18494  isnzr2hash  20287  mplcoe5lem  21576  ioovolcl  25069  elply2  25692  cusgrsize  28691  rusgrpropedg  28821  wlkonprop  28895  wksonproplem  28941  wksonproplemOLD  28942  pthdlem1  29003  3oalem1  30893  elorrvc  33400  ballotlemfc0  33429  ballotlemfcc  33430  ballotlemodife  33434  ballotth  33474  nummin  34032  opnrebl2  35144  bj-eldiag2  35996  topdifinffinlem  36166  finxpsuc  36217  wl-ax11-lem3  36387  matunitlindflem2  36423  matunitlindf  36424  poimirlem28  36454  poimirlem29  36455  mblfinlem1  36463  ovoliunnfl  36468  voliunnfl  36470  itg2addnclem2  36478  areacirclem5  36518  seqpo  36553  incsequz  36554  incsequz2  36555  ismtycnv  36608  prnc  36873  dihatexv2  40148  isdomn4  40970  sn-sup2  41286  prjspval  41289  tfsconcatlem  42019  omssrncard  42224  reabsifneg  42316  reabsifnpos  42317  reabsifpos  42318  reabsifnneg  42319  fperiodmullem  43948  climsuselem1  44258  climsuse  44259  0ellimcdiv  44300  fperdvper  44570  iblsplit  44617  stirlinglem11  44735  qndenserrnbllem  44945  sge0fodjrnlem  45067  upwlkbprop  46451  c0rnghm  46646  regt1loggt0  47124