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  2665  festino  2674  baroco  2676  moeq3  3718  sbcimdv  3859  ssel  3977  sscon  4143  uniss  4915  trel3  5269  axprlem4  5426  ssopab2  5551  coss1  5866  fununi  6641  imadif  6650  fss  6752  ssimaex  6994  ssoprab2  7501  poxp  8153  soxp  8154  poseq  8183  suppofssd  8228  pmss12g  8909  ss2ixp  8950  xpdom2  9107  fisup2g  9508  fisupcl  9509  fiinf2g  9540  inf3lem1  9668  epfrs  9771  cfub  10289  cflm  10290  fin23lem34  10386  isf32lem2  10394  axcc4  10479  domtriomlem  10482  ltexprlem3  11078  nnunb  12522  indstr  12958  qbtwnxr  13242  qsqueeze  13243  xrsupsslem  13349  xrinfmsslem  13350  ioc0  13434  climshftlem  15610  o1rlimmul  15655  ramub2  17052  monmat2matmon  22830  tgcl  22976  neips  23121  ssnei2  23124  tgcnp  23261  cnpnei  23272  cnpco  23275  hauscmplem  23414  hauscmp  23415  llyss  23487  nllyss  23488  lfinun  23533  kgen2ss  23563  txcnpi  23616  txcmplem1  23649  fgss  23881  cnpflf2  24008  fclsss1  24030  fclscf  24033  alexsubALT  24059  cnextcn  24075  tsmsxp  24163  mopni3  24507  psmetutop  24580  tngngp3  24677  iscau4  25313  caussi  25331  ovolgelb  25515  mbfi1flim  25758  ellimc3  25914  lhop1  26053  tgbtwndiff  28514  axcontlem4  28982  clwwlknonwwlknonb  30125  sspmval  30752  shmodsi  31408  atcvat4i  32416  cdj3lem2b  32456  ifeqeqx  32555  acunirnmpt  32669  xrge0infss  32764  constrextdg2lem  33789  crefss  33848  issgon  34124  cvmlift2lem12  35319  satfv1  35368  satfvsucsuc  35370  ss2mcls  35573  btwndiff  36028  seglecgr12im  36111  fnessref  36358  waj-ax  36415  lukshef-ax2  36416  bj-isrvec  37295  icorempo  37352  finxpreclem1  37390  fvineqsneq  37413  pibt2  37418  tan2h  37619  poimirlem31  37658  poimir  37660  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  cvrat4  39445  athgt  39458  ps-2  39480  paddss1  39819  paddss2  39820  cdlemg33b0  40703  cdlemg33a  40708  dihjat1lem  41430  fphpdo  42828  irrapxlem2  42834  pell14qrss1234  42867  pell1qrss14  42879  acongtr  42990  ofoaid1  43371  ofoaid2  43372  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  grumnudlem  44304  ax6e2eq  44577  modelaxreplem1  44995  islptre  45634  limccog  45635  grilcbri2  47971  opnneilv  48806