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  3103  2reu1  3854  difrab  4274  rabsnifsb  4693  foconst  6814  elfvmptrab  7026  dffo4  7105  dffo5  7106  isofrlem  7349  brfvopab  7480  onint  7798  el2mpocl  8090  suppofssd  8208  tz7.48lem  8437  opthreg  9597  eltsk2g  10754  recgt1i  12130  sup2  12189  elnnnn0c  12567  elnnz1  12638  recnz  12689  eluz2b2  12963  iccsplit  13530  elfzp12  13650  1mod  13956  pfxsuff1eqwrdeq  14760  cos01gt0  16272  oddnn02np1  16431  reumodprminv  16889  clatl  18589  isacs4lem  18625  isacs5lem  18626  isnzr2hash  20647  c0rnghm  20664  isdomn4  20844  mplcoe5lem  22220  ioovolcl  25759  elply2  26383  cusgrsize  29834  rusgrpropedg  29964  wlkonprop  30036  wksonproplem  30082  pthdlem1  30145  3oalem1  32044  elorrvc  34878  ballotlemfc0  34907  ballotlemfcc  34908  ballotlemodife  34912  ballotth  34952  nummin  35501  opnrebl2  36865  bj-eldiag2  37854  topdifinffinlem  38026  finxpsuc  38077  matunitlindflem2  38301  matunitlindf  38302  poimirlem28  38332  poimirlem29  38333  mblfinlem1  38341  ovoliunnfl  38346  voliunnfl  38348  itg2addnclem2  38356  areacirclem5  38396  seqpo  38431  incsequz  38432  incsequz2  38433  ismtycnv  38486  prnc  38751  dihatexv2  42146  unitscyglem4  42998  sn-sup2  43298  prjspval  43368  tfsconcatlem  44096  omssrncard  44299  reabsifneg  44391  reabsifnpos  44392  reabsifpos  44393  reabsifnneg  44394  relpfrlem  45695  fperiodmullem  46055  climsuselem1  46356  climsuse  46357  0ellimcdiv  46396  fperdvper  46666  iblsplit  46713  stirlinglem11  46831  qndenserrnbllem  47041  sge0fodjrnlem  47163  upwlkbprop  48936  regt1loggt0  49349