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  3067  2reu1  3843  difrab  4265  rabsnifsb  4672  foconst  6750  elfvmptrab  6958  dffo4  7036  dffo5  7037  isofrlem  7274  brfvopab  7403  onint  7723  el2mpocl  8016  suppofssd  8133  tz7.48lem  8360  opthreg  9508  eltsk2g  10642  recgt1i  12019  sup2  12078  elnnnn0c  12426  elnnz1  12498  recnz  12548  eluz2b2  12819  iccsplit  13385  elfzp12  13503  1mod  13807  pfxsuff1eqwrdeq  14606  cos01gt0  16100  oddnn02np1  16259  reumodprminv  16716  clatl  18414  isacs4lem  18450  isacs5lem  18451  isnzr2hash  20434  c0rnghm  20450  isdomn4  20631  mplcoe5lem  21974  ioovolcl  25498  elply2  26128  cusgrsize  29433  rusgrpropedg  29563  wlkonprop  29635  wksonproplem  29681  pthdlem1  29744  3oalem1  31642  elorrvc  34477  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemodife  34511  ballotth  34551  nummin  35104  opnrebl2  36365  bj-eldiag2  37221  topdifinffinlem  37391  finxpsuc  37442  matunitlindflem2  37656  matunitlindf  37657  poimirlem28  37687  poimirlem29  37688  mblfinlem1  37696  ovoliunnfl  37701  voliunnfl  37703  itg2addnclem2  37711  areacirclem5  37751  seqpo  37786  incsequz  37787  incsequz2  37788  ismtycnv  37841  prnc  38106  dihatexv2  41437  unitscyglem4  42290  sn-sup2  42583  prjspval  42695  tfsconcatlem  43428  omssrncard  43632  reabsifneg  43724  reabsifnpos  43725  reabsifpos  43726  reabsifnneg  43727  relpfrlem  45045  fperiodmullem  45403  climsuselem1  45706  climsuse  45707  0ellimcdiv  45746  fperdvper  46016  iblsplit  46063  stirlinglem11  46181  qndenserrnbllem  46391  sge0fodjrnlem  46513  upwlkbprop  48237  regt1loggt0  48636