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  3064  2reu1  3851  difrab  4271  rabsnifsb  4676  foconst  6755  elfvmptrab  6963  dffo4  7041  dffo5  7042  isofrlem  7281  brfvopab  7410  onint  7730  el2mpocl  8026  suppofssd  8143  tz7.48lem  8370  opthreg  9533  eltsk2g  10664  recgt1i  12040  sup2  12099  elnnnn0c  12447  elnnz1  12519  recnz  12569  eluz2b2  12840  iccsplit  13406  elfzp12  13524  1mod  13825  pfxsuff1eqwrdeq  14623  cos01gt0  16118  oddnn02np1  16277  reumodprminv  16734  clatl  18432  isacs4lem  18468  isacs5lem  18469  isnzr2hash  20422  c0rnghm  20438  isdomn4  20619  mplcoe5lem  21962  ioovolcl  25487  elply2  26117  cusgrsize  29418  rusgrpropedg  29548  wlkonprop  29620  wksonproplem  29666  pthdlem1  29729  3oalem1  31624  elorrvc  34434  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemodife  34468  ballotth  34508  nummin  35060  opnrebl2  36297  bj-eldiag2  37153  topdifinffinlem  37323  finxpsuc  37374  wl-ax11-lem3  37563  matunitlindflem2  37599  matunitlindf  37600  poimirlem28  37630  poimirlem29  37631  mblfinlem1  37639  ovoliunnfl  37644  voliunnfl  37646  itg2addnclem2  37654  areacirclem5  37694  seqpo  37729  incsequz  37730  incsequz2  37731  ismtycnv  37784  prnc  38049  dihatexv2  41321  unitscyglem4  42174  sn-sup2  42467  prjspval  42579  tfsconcatlem  43312  omssrncard  43516  reabsifneg  43608  reabsifnpos  43609  reabsifpos  43610  reabsifnneg  43611  relpfrlem  44930  fperiodmullem  45288  climsuselem1  45592  climsuse  45593  0ellimcdiv  45634  fperdvper  45904  iblsplit  45951  stirlinglem11  46069  qndenserrnbllem  46279  sge0fodjrnlem  46401  upwlkbprop  48126  regt1loggt0  48525