Theorem anim2d 612

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  darii  2659  festino  2668  baroco  2670  moeq3  3669  sbcimdv  3808  ssel  3926  sscon  4091  uniss  4865  trel3  5205  axprlem4  5362  ssopab2  5484  coss1  5793  fununi  6552  imadif  6561  fss  6663  ssimaex  6902  ssoprab2  7409  poxp  8053  soxp  8054  poseq  8083  suppofssd  8128  pmss12g  8788  ss2ixp  8829  xpdom2  8980  fisup2g  9348  fisupcl  9349  fiinf2g  9381  elirrv  9478  inf3lem1  9513  epfrs  9616  cfub  10132  cflm  10133  fin23lem34  10229  isf32lem2  10237  axcc4  10322  domtriomlem  10325  ltexprlem3  10921  nnunb  12369  indstr  12806  qbtwnxr  13091  qsqueeze  13092  xrsupsslem  13198  xrinfmsslem  13199  ioc0  13284  climshftlem  15473  o1rlimmul  15518  ramub2  16918  chnrss  18513  monmat2matmon  22732  tgcl  22877  neips  23021  ssnei2  23024  tgcnp  23161  cnpnei  23172  cnpco  23175  hauscmplem  23314  hauscmp  23315  llyss  23387  nllyss  23388  lfinun  23433  kgen2ss  23463  txcnpi  23516  txcmplem1  23549  fgss  23781  cnpflf2  23908  fclsss1  23930  fclscf  23933  alexsubALT  23959  cnextcn  23975  tsmsxp  24063  mopni3  24402  psmetutop  24475  tngngp3  24564  iscau4  25199  caussi  25217  ovolgelb  25401  mbfi1flim  25644  ellimc3  25800  lhop1  25939  tgbtwndiff  28477  axcontlem4  28938  clwwlknonwwlknonb  30076  sspmval  30703  shmodsi  31359  atcvat4i  32367  cdj3lem2b  32407  ifeqeqx  32512  acunirnmpt  32631  xrge0infss  32733  constrextdg2lem  33751  crefss  33852  issgon  34126  cvmlift2lem12  35326  satfv1  35375  satfvsucsuc  35377  ss2mcls  35580  btwndiff  36040  seglecgr12im  36123  fnessref  36370  waj-ax  36427  lukshef-ax2  36428  bj-isrvec  37307  icorempo  37364  finxpreclem1  37402  fvineqsneq  37425  pibt2  37430  tan2h  37631  poimirlem31  37670  poimir  37672  mblfinlem3  37678  mblfinlem4  37679  ismblfin  37680  cvrat4  39461  athgt  39474  ps-2  39496  paddss1  39835  paddss2  39836  cdlemg33b0  40719  cdlemg33a  40724  dihjat1lem  41446  fphpdo  42829  irrapxlem2  42835  pell14qrss1234  42868  pell1qrss14  42880  acongtr  42990  ofoaid1  43370  ofoaid2  43371  fzunt  43467  fzuntd  43468  fzunt1d  43469  fzuntgd  43470  grumnudlem  44297  ax6e2eq  44569  modelaxreplem1  44990  islptre  45638  limccog  45639  grilcbri2  48021  opnneilv  48919