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  3097  2reu1  3844  difrab  4263  rabsnifsb  4679  foconst  6812  elfvmptrab  7024  dffo4  7104  dffo5  7105  isofrlem  7349  brfvopab  7478  onint  7805  el2mpocl  8098  suppofssd  8224  tz7.48lemOLD  8455  opthreg  9623  eltsk2g  10840  recgt1i  12218  sup2  12277  elnnnn0c  12655  elnnz1  12726  recnz  12778  eluz2b2  13052  iccsplit  13620  elfzp12  13741  1mod  14047  pfxsuff1eqwrdeq  14853  cos01gt0  16365  oddnn02np1  16524  reumodprminv  16988  clatl  18688  isacs4lem  18724  isacs5lem  18725  isnzr2hash  20776  c0rnghm  20793  isdomn4  20973  mplcoe5lem  22354  matunitlindflem2  23001  matunitlindf  23002  ioovolcl  25897  elply2  26520  cusgrsize  30041  rusgrpropedg  30171  wlkonprop  30243  wksonproplem  30293  pthdlem1  30358  3oalem1  32270  elorrvc  35143  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemodife  35177  ballotth  35217  nummin  35775  opnrebl2  37202  bj-eldiag2  38192  topdifinffinlem  38364  finxpsuc  38415  poimirlem28  38660  poimirlem29  38661  mblfinlem1  38669  ovoliunnfl  38674  voliunnfl  38676  itg2addnclem2  38684  areacirclem5  38724  seqpo  38775  incsequz  38776  incsequz2  38777  ismtycnv  38830  prnc  39095  dihatexv2  42490  unitscyglem4  43342  sn-sup2  43649  prjspval  43725  tfsconcatlem  44432  omssrncard  44635  reabsifneg  44726  reabsifnpos  44727  reabsifpos  44728  reabsifnneg  44729  relpfrlem  46037  fperiodmullem  46413  climsuselem1  46713  climsuse  46714  0ellimcdiv  46753  fperdvper  47023  iblsplit  47070  stirlinglem11  47188  qndenserrnbllem  47398  sge0fodjrnlem  47520  upwlkbprop  49330  regt1loggt0  49742