Theorem anim2d 624

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
anim2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 621	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:  darii  2689  festino  2698  baroco  2700  moeq3  3669  sbcimdv  3806  ssel  3902  sscon  4079  uniss  4874  trel3  5220  axprlem4  5387  ssopab2  5520  coss1  5832  fununi  6615  imadif  6624  fss  6726  ssimaex  6970  ssoprab2  7488  poxp  8140  soxp  8141  poseq  8175  suppofssd  8221  pmss12g  8898  ss2ixp  8939  xpdom2  9092  fisup2g  9462  fisupcl  9463  fiinf2g  9495  elirrvOLD  9593  inf3lem1  9630  epfrs  9733  cfub  10327  cflm  10328  fin23lem34  10425  isf32lem2  10433  axcc4  10518  domtriomlem  10521  ltexprlem3  11124  nnunb  12603  indstr  13044  qbtwnxr  13331  qsqueeze  13332  xrsupsslem  13438  xrinfmsslem  13439  ioc0  13524  climshftlem  15742  o1rlimmul  15787  ramub2  17193  chnrss  18790  monmat2matmon  23143  tgcl  23288  neips  23432  ssnei2  23435  tgcnp  23572  cnpnei  23583  cnpco  23586  hauscmplem  23725  hauscmp  23726  llyss  23799  nllyss  23800  lfinun  23845  kgen2ss  23875  txcnpi  23928  txcmplem1  23961  fgss  24193  cnpflf2  24320  fclsss1  24342  fclscf  24345  alexsubALT  24371  cnextcn  24387  tsmsxp  24475  mopni3  24814  psmetutop  24887  tngngp3  24976  iscau4  25601  caussi  25619  ovolgelb  25802  mbfi1flim  26045  ellimc3  26200  lhop1  26335  tgbtwndiff  28970  axcontlem4  29546  clwwlknonwwlknonb  30698  sspmval  31336  shmodsi  31992  atcvat4i  33000  cdj3lem2b  33040  ifeqeqx  33181  acunirnmpt  33296  xrge0infss  33395  constrextdg2lem  34423  crefss  34524  issgon  34798  r1omhfb  35783  r1omhfbregs  35854  cvmlift2lem12  36148  satfv1  36197  satfvsucsuc  36199  ss2mcls  36402  btwndiff  36867  seglecgr12im  36950  fnessref  37220  waj-ax  37277  lukshef-ax2  37278  bj-isrvec  38291  icorempo  38350  finxpreclem1  38388  fvineqsneq  38411  pibt2  38416  wl-dfcleq  38513  tan2h  38611  poimirlem31  38645  poimir  38647  mblfinlem3  38653  mblfinlem4  38654  ismblfin  38655  cvrat4  40576  athgt  40589  ps-2  40611  paddss1  40950  paddss2  40951  cdlemg33b0  41834  cdlemg33a  41839  dihjat1lem  42561  fphpdo  43900  irrapxlem2  43906  pell14qrss1234  43939  pell1qrss14  43951  acongtr  44061  ofoaid1  44436  ofoaid2  44437  fzunt  44532  fzuntd  44533  fzunt1d  44534  fzuntgd  44535  grumnudlem  45345  ax6e2eq  45616  modelaxreplem1  46044  islptre  46707  limccog  46708  grilcbri2  49185  opnneilv  50093