Theorem imdistani 578

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 564	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 411	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syldanl  613  cases2ALT  1064  reximia  3100  2reu1  3852  difrab  4272  rabsnifsb  4689  foconst  6809  elfvmptrab  7021  dffo4  7100  dffo5  7101  isofrlem  7340  brfvopab  7469  onint  7790  el2mpocl  8082  suppofssd  8200  tz7.48lem  8429  opthreg  9588  eltsk2g  10737  recgt1i  12113  sup2  12172  elnnnn0c  12550  elnnz1  12621  recnz  12672  eluz2b2  12946  iccsplit  13513  elfzp12  13633  1mod  13938  pfxsuff1eqwrdeq  14738  cos01gt0  16248  oddnn02np1  16407  reumodprminv  16865  clatl  18565  isacs4lem  18601  isacs5lem  18602  isnzr2hash  20604  c0rnghm  20621  isdomn4  20801  mplcoe5lem  22171  ioovolcl  25710  elply2  26334  cusgrsize  29785  rusgrpropedg  29915  wlkonprop  29987  wksonproplem  30033  pthdlem1  30096  3oalem1  31995  elorrvc  34835  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemodife  34869  ballotth  34909  nummin  35465  opnrebl2  36813  bj-eldiag2  37802  topdifinffinlem  37974  finxpsuc  38025  matunitlindflem2  38249  matunitlindf  38250  poimirlem28  38280  poimirlem29  38281  mblfinlem1  38289  ovoliunnfl  38294  voliunnfl  38296  itg2addnclem2  38304  areacirclem5  38344  seqpo  38379  incsequz  38380  incsequz2  38381  ismtycnv  38434  prnc  38699  dihatexv2  42094  unitscyglem4  42946  sn-sup2  43246  prjspval  43318  tfsconcatlem  44046  omssrncard  44249  reabsifneg  44341  reabsifnpos  44342  reabsifpos  44343  reabsifnneg  44344  relpfrlem  45645  fperiodmullem  46005  climsuselem1  46306  climsuse  46307  0ellimcdiv  46346  fperdvper  46616  iblsplit  46663  stirlinglem11  46781  qndenserrnbllem  46991  sge0fodjrnlem  47113  upwlkbprop  48886  regt1loggt0  49299