Theorem anim2d 613

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 610	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sbimdvOLD  2516  sbimdOLD  2518  darii  2750  festino  2759  baroco  2761  moeq3  3705  ssel  3963  sscon  4117  uniss  4848  trel3  5182  ssopab2  5435  coss1  5728  fununi  6431  imadif  6440  fss  6529  ssimaex  6750  ssoprab2  7224  poxp  7824  soxp  7825  suppofssd  7869  pmss12g  8435  ss2ixp  8476  xpdom2  8614  fisup2g  8934  fisupcl  8935  fiinf2g  8966  inf3lem1  9093  epfrs  9175  cfub  9673  cflm  9674  fin23lem34  9770  isf32lem2  9778  axcc4  9863  domtriomlem  9866  ltexprlem3  10462  nnunb  11896  indstr  12319  qbtwnxr  12596  qsqueeze  12597  xrsupsslem  12703  xrinfmsslem  12704  ioc0  12788  climshftlem  14933  o1rlimmul  14977  ramub2  16352  monmat2matmon  21434  tgcl  21579  neips  21723  ssnei2  21726  tgcnp  21863  cnpnei  21874  cnpco  21877  hauscmplem  22016  hauscmp  22017  llyss  22089  nllyss  22090  lfinun  22135  kgen2ss  22165  txcnpi  22218  txcmplem1  22251  fgss  22483  cnpflf2  22610  fclsss1  22632  fclscf  22635  alexsubALT  22661  cnextcn  22677  tsmsxp  22765  mopni3  23106  psmetutop  23179  tngngp3  23267  iscau4  23884  caussi  23902  ovolgelb  24083  mbfi1flim  24326  ellimc3  24479  lhop1  24613  tgbtwndiff  26294  axcontlem4  26755  clwwlknonwwlknonb  27887  sspmval  28512  shmodsi  29168  atcvat4i  30176  cdj3lem2b  30216  ifeqeqx  30299  acunirnmpt  30406  xrge0infss  30486  crefss  31115  issgon  31384  cvmlift2lem12  32563  satfv1  32612  satfvsucsuc  32614  ss2mcls  32817  poseq  33097  btwndiff  33490  seglecgr12im  33573  fnessref  33707  waj-ax  33764  lukshef-ax2  33765  icorempo  34634  finxpreclem1  34672  fvineqsneq  34695  pibt2  34700  tan2h  34886  poimirlem31  34925  poimir  34927  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  cvrat4  36581  athgt  36594  ps-2  36616  paddss1  36955  paddss2  36956  cdlemg33b0  37839  cdlemg33a  37844  dihjat1lem  38566  fphpdo  39421  irrapxlem2  39427  pell14qrss1234  39460  pell1qrss14  39472  acongtr  39582  grumnudlem  40628  ax6e2eq  40898  islptre  41907  limccog  41908