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  603  cases2ALT  1049  reximia  3072  2reu1  3835  difrab  4258  rabsnifsb  4666  foconst  6767  elfvmptrab  6977  dffo4  7055  dffo5  7056  isofrlem  7295  brfvopab  7424  onint  7744  el2mpocl  8036  suppofssd  8153  tz7.48lem  8380  opthreg  9539  eltsk2g  10674  recgt1i  12053  sup2  12112  elnnnn0c  12482  elnnz1  12553  recnz  12604  eluz2b2  12871  iccsplit  13438  elfzp12  13557  1mod  13862  pfxsuff1eqwrdeq  14661  cos01gt0  16158  oddnn02np1  16317  reumodprminv  16775  clatl  18474  isacs4lem  18510  isacs5lem  18511  isnzr2hash  20496  c0rnghm  20512  isdomn4  20693  mplcoe5lem  22017  ioovolcl  25537  elply2  26161  cusgrsize  29523  rusgrpropedg  29653  wlkonprop  29725  wksonproplem  29771  pthdlem1  29834  3oalem1  31733  elorrvc  34608  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemodife  34642  ballotth  34682  nummin  35236  opnrebl2  36503  bj-eldiag2  37491  topdifinffinlem  37663  finxpsuc  37714  matunitlindflem2  37938  matunitlindf  37939  poimirlem28  37969  poimirlem29  37970  mblfinlem1  37978  ovoliunnfl  37983  voliunnfl  37985  itg2addnclem2  37993  areacirclem5  38033  seqpo  38068  incsequz  38069  incsequz2  38070  ismtycnv  38123  prnc  38388  dihatexv2  41785  unitscyglem4  42637  sn-sup2  42936  prjspval  43036  tfsconcatlem  43764  omssrncard  43967  reabsifneg  44059  reabsifnpos  44060  reabsifpos  44061  reabsifnneg  44062  relpfrlem  45380  fperiodmullem  45736  climsuselem1  46037  climsuse  46038  0ellimcdiv  46077  fperdvper  46347  iblsplit  46394  stirlinglem11  46512  qndenserrnbllem  46722  sge0fodjrnlem  46844  upwlkbprop  48614  regt1loggt0  49012