Theorem imdistani 579

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syldanl  614  cases2ALT  1064  reximia  3101  2reu1  3849  difrab  4266  rabsnifsb  4683  foconst  6836  elfvmptrab  7049  dffo4  7130  dffo5  7131  isofrlem  7374  brfvopab  7503  onint  7831  el2mpocl  8125  suppofssd  8251  tz7.48lemOLD  8482  opthreg  9649  eltsk2g  10866  recgt1i  12244  sup2  12303  elnnnn0c  12681  elnnz1  12752  recnz  12804  eluz2b2  13078  iccsplit  13646  elfzp12  13767  1mod  14073  pfxsuff1eqwrdeq  14879  cos01gt0  16391  oddnn02np1  16550  reumodprminv  17014  clatl  18714  isacs4lem  18750  isacs5lem  18751  isnzr2hash  20803  c0rnghm  20820  isdomn4  21000  mplcoe5lem  22381  matunitlindflem2  23028  matunitlindf  23029  ioovolcl  25924  elply2  26547  cusgrsize  30068  rusgrpropedg  30198  wlkonprop  30270  wksonproplem  30320  pthdlem1  30385  3oalem1  32297  elorrvc  35179  ballotlemfc0  35208  ballotlemfcc  35209  ballotlemodife  35213  ballotth  35253  nummin  35819  opnrebl2  37300  bj-eldiag2  38303  topdifinffinlem  38475  finxpsuc  38526  poimirlem28  38771  poimirlem29  38772  mblfinlem1  38780  ovoliunnfl  38785  voliunnfl  38787  itg2addnclem2  38795  areacirclem5  38835  seqpo  38884  incsequz  38885  incsequz2  38886  ismtycnv  38939  prnc  39204  dihatexv2  42599  unitscyglem4  43451  sn-sup2  43759  prjspval  43835  tfsconcatlem  44541  omssrncard  44744  reabsifneg  44835  reabsifnpos  44836  reabsifpos  44837  reabsifnneg  44838  relpfrlem  46149  fperiodmullem  46534  climsuselem1  46834  climsuse  46835  0ellimcdiv  46874  fperdvper  47144  iblsplit  47191  stirlinglem11  47309  qndenserrnbllem  47519  sge0fodjrnlem  47641  upwlkbprop  49451  regt1loggt0  49863