Theorem anim2d 588

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 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 585	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  moeq3  3416  ssel  3630  sscon  3777  uniss  4490  trel3  4793  ssopab2  5030  coss1  5310  fununi  6002  imadif  6011  fss  6094  ssimaex  6302  ssoprab2  6753  poxp  7334  soxp  7335  pmss12g  7926  ss2ixp  7963  xpdom2  8096  fisup2g  8415  fisupcl  8416  fiinf2g  8447  inf3lem1  8563  epfrs  8645  cfub  9109  cflm  9110  fin23lem34  9206  isf32lem2  9214  axcc4  9299  domtriomlem  9302  ltexprlem3  9898  nnunb  11326  indstr  11794  qbtwnxr  12069  qsqueeze  12070  xrsupsslem  12175  xrinfmsslem  12176  ioc0  12260  climshftlem  14349  o1rlimmul  14393  ramub2  15765  monmat2matmon  20677  tgcl  20821  neips  20965  ssnei2  20968  tgcnp  21105  cnpnei  21116  cnpco  21119  hauscmplem  21257  hauscmp  21258  llyss  21330  nllyss  21331  lfinun  21376  kgen2ss  21406  txcnpi  21459  txcmplem1  21492  fgss  21724  cnpflf2  21851  fclsss1  21873  fclscf  21876  alexsubALT  21902  cnextcn  21918  tsmsxp  22005  mopni3  22346  psmetutop  22419  tngngp3  22507  iscau4  23123  caussi  23141  ovolgelb  23294  mbfi1flim  23535  ellimc3  23688  lhop1  23822  tgbtwndiff  25446  axcontlem4  25892  sspmval  27716  shmodsi  28376  atcvat4i  29384  cdj3lem2b  29424  ifeqeqx  29487  acunirnmpt  29587  xrge0infss  29653  crefss  30044  issgon  30314  cvmlift2lem12  31422  ss2mcls  31591  poseq  31878  btwndiff  32259  seglecgr12im  32342  fnessref  32477  waj-ax  32538  lukshef-ax2  32539  icorempt2  33329  finxpreclem1  33356  tan2h  33531  poimirlem31  33570  poimir  33572  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  cvrat4  35047  athgt  35060  ps-2  35082  paddss1  35421  paddss2  35422  cdlemg33b0  36306  cdlemg33a  36311  dihjat1lem  37034  fphpdo  37698  irrapxlem2  37704  pell14qrss1234  37737  pell1qrss14  37749  acongtr  37862  ax6e2eq  39090  islptre  40169  limccog  40170