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  3848  difrab  4268  rabsnifsb  4675  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  20435  c0rnghm  20451  isdomn4  20632  mplcoe5lem  21975  ioovolcl  25499  elply2  26129  cusgrsize  29434  rusgrpropedg  29564  wlkonprop  29636  wksonproplem  29682  pthdlem1  29745  3oalem1  31640  elorrvc  34475  ballotlemfc0  34504  ballotlemfcc  34505  ballotlemodife  34509  ballotth  34549  nummin  35102  opnrebl2  36361  bj-eldiag2  37217  topdifinffinlem  37387  finxpsuc  37438  wl-ax11-lem3  37627  matunitlindflem2  37663  matunitlindf  37664  poimirlem28  37694  poimirlem29  37695  mblfinlem1  37703  ovoliunnfl  37708  voliunnfl  37710  itg2addnclem2  37718  areacirclem5  37758  seqpo  37793  incsequz  37794  incsequz2  37795  ismtycnv  37848  prnc  38113  dihatexv2  41384  unitscyglem4  42237  sn-sup2  42530  prjspval  42642  tfsconcatlem  43375  omssrncard  43579  reabsifneg  43671  reabsifnpos  43672  reabsifpos  43673  reabsifnneg  43674  relpfrlem  44992  fperiodmullem  45350  climsuselem1  45653  climsuse  45654  0ellimcdiv  45693  fperdvper  45963  iblsplit  46010  stirlinglem11  46128  qndenserrnbllem  46338  sge0fodjrnlem  46460  upwlkbprop  48175  regt1loggt0  48574