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  3073  2reu1  3849  difrab  4272  rabsnifsb  4681  foconst  6769  elfvmptrab  6979  dffo4  7057  dffo5  7058  isofrlem  7296  brfvopab  7425  onint  7745  el2mpocl  8038  suppofssd  8155  tz7.48lem  8382  opthreg  9539  eltsk2g  10674  recgt1i  12051  sup2  12110  elnnnn0c  12458  elnnz1  12529  recnz  12579  eluz2b2  12846  iccsplit  13413  elfzp12  13531  1mod  13835  pfxsuff1eqwrdeq  14634  cos01gt0  16128  oddnn02np1  16287  reumodprminv  16744  clatl  18443  isacs4lem  18479  isacs5lem  18480  isnzr2hash  20464  c0rnghm  20480  isdomn4  20661  mplcoe5lem  22006  ioovolcl  25539  elply2  26169  cusgrsize  29540  rusgrpropedg  29670  wlkonprop  29742  wksonproplem  29788  pthdlem1  29851  3oalem1  31749  elorrvc  34641  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemodife  34675  ballotth  34715  nummin  35268  opnrebl2  36534  bj-eldiag2  37429  topdifinffinlem  37599  finxpsuc  37650  matunitlindflem2  37865  matunitlindf  37866  poimirlem28  37896  poimirlem29  37897  mblfinlem1  37905  ovoliunnfl  37910  voliunnfl  37912  itg2addnclem2  37920  areacirclem5  37960  seqpo  37995  incsequz  37996  incsequz2  37997  ismtycnv  38050  prnc  38315  dihatexv2  41712  unitscyglem4  42565  sn-sup2  42858  prjspval  42958  tfsconcatlem  43690  omssrncard  43893  reabsifneg  43985  reabsifnpos  43986  reabsifpos  43987  reabsifnneg  43988  relpfrlem  45306  fperiodmullem  45662  climsuselem1  45964  climsuse  45965  0ellimcdiv  46004  fperdvper  46274  iblsplit  46321  stirlinglem11  46439  qndenserrnbllem  46649  sge0fodjrnlem  46771  upwlkbprop  48495  regt1loggt0  48893