Theorem anim2d 587

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 584	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 196  df-an 385

This theorem is referenced by:  eleq2dOLD  2674  moeq3  3350  ssel  3562  sscon  3706  uniss  4389  trel3  4683  ssopab2  4916  coss1  5187  fununi  5864  imadif  5873  fss  5955  ssimaex  6158  ssoprab2  6587  poxp  7154  soxp  7155  pmss12g  7748  ss2ixp  7785  xpdom2  7918  fisup2g  8235  fisupcl  8236  fiinf2g  8267  inf3lem1  8386  epfrs  8468  cfub  8932  cflm  8933  fin23lem34  9029  isf32lem2  9037  axcc4  9122  domtriomlem  9125  ltexprlem3  9717  nnunb  11138  indstr  11591  qbtwnxr  11867  qsqueeze  11868  xrsupsslem  11968  xrinfmsslem  11969  ioc0  12052  climshftlem  14102  o1rlimmul  14146  ramub2  15505  monmat2matmon  20396  tgcl  20532  neips  20675  ssnei2  20678  tgcnp  20815  cnpnei  20826  cnpco  20829  hauscmplem  20967  hauscmp  20968  llyss  21040  nllyss  21041  lfinun  21086  kgen2ss  21116  txcnpi  21169  txcmplem1  21202  fgss  21435  cnpflf2  21562  fclsss1  21584  fclscf  21587  alexsubALT  21613  cnextcn  21629  tsmsxp  21716  mopni3  22057  psmetutop  22130  tngngp3  22218  iscau4  22830  caussi  22848  ovolgelb  23000  mbfi1flim  23241  ellimc3  23394  lhop1  23526  tgbtwndiff  25146  axcontlem4  25593  iswlkg  25846  sspmval  26766  shmodsi  27426  atcvat4i  28434  cdj3lem2b  28474  ifeqeqx  28539  acunirnmpt  28635  xrge0infss  28709  crefss  29038  issgon  29307  cvmlift2lem12  30344  ss2mcls  30513  poseq  30788  btwndiff  31098  seglecgr12im  31181  fnessref  31316  waj-ax  31377  lukshef-ax2  31378  icorempt2  32169  finxpreclem1  32196  tan2h  32365  poimirlem31  32404  poimir  32406  mblfinlem3  32412  mblfinlem4  32413  ismblfin  32414  cvrat4  33541  athgt  33554  ps-2  33576  paddss1  33915  paddss2  33916  cdlemg33b0  34801  cdlemg33a  34806  dihjat1lem  35529  fphpdo  36193  irrapxlem2  36199  pell14qrss1234  36232  pell1qrss14  36244  acongtr  36357  ax6e2eq  37588  islptre  38480  limccog  38481