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  602  cases2ALT  1048  reximia  3078  2reu1  3905  difrab  4323  rabsnifsb  4726  foconst  6835  elfvmptrab  7044  dffo4  7122  dffo5  7123  isofrlem  7359  brfvopab  7489  onint  7809  el2mpocl  8109  suppofssd  8226  tz7.48lem  8479  opthreg  9655  eltsk2g  10788  recgt1i  12162  sup2  12221  elnnnn0c  12568  elnnz1  12640  recnz  12690  eluz2b2  12960  iccsplit  13521  elfzp12  13639  1mod  13939  pfxsuff1eqwrdeq  14733  cos01gt0  16223  oddnn02np1  16381  reumodprminv  16837  clatl  18565  isacs4lem  18601  isacs5lem  18602  isnzr2hash  20535  c0rnghm  20551  isdomn4  20732  mplcoe5lem  22074  ioovolcl  25618  elply2  26249  cusgrsize  29486  rusgrpropedg  29616  wlkonprop  29690  wksonproplem  29736  wksonproplemOLD  29737  pthdlem1  29798  3oalem1  31690  elorrvc  34444  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemodife  34478  ballotth  34518  nummin  35083  opnrebl2  36303  bj-eldiag2  37159  topdifinffinlem  37329  finxpsuc  37380  wl-ax11-lem3  37567  matunitlindflem2  37603  matunitlindf  37604  poimirlem28  37634  poimirlem29  37635  mblfinlem1  37643  ovoliunnfl  37648  voliunnfl  37650  itg2addnclem2  37658  areacirclem5  37698  seqpo  37733  incsequz  37734  incsequz2  37735  ismtycnv  37788  prnc  38053  dihatexv2  41321  unitscyglem4  42179  sn-sup2  42477  prjspval  42589  tfsconcatlem  43325  omssrncard  43529  reabsifneg  43621  reabsifnpos  43622  reabsifpos  43623  reabsifnneg  43624  fperiodmullem  45253  climsuselem1  45562  climsuse  45563  0ellimcdiv  45604  fperdvper  45874  iblsplit  45921  stirlinglem11  46039  qndenserrnbllem  46249  sge0fodjrnlem  46371  upwlkbprop  47981  regt1loggt0  48385