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  2658  festino  2667  baroco  2669  moeq3  3674  sbcimdv  3813  ssel  3931  sscon  4096  uniss  4869  trel3  5211  axprlem4  5368  ssopab2  5493  coss1  5802  fununi  6561  imadif  6570  fss  6672  ssimaex  6912  ssoprab2  7421  poxp  8068  soxp  8069  poseq  8098  suppofssd  8143  pmss12g  8803  ss2ixp  8844  xpdom2  8996  fisup2g  9378  fisupcl  9379  fiinf2g  9411  elirrv  9508  inf3lem1  9543  epfrs  9646  cfub  10162  cflm  10163  fin23lem34  10259  isf32lem2  10267  axcc4  10352  domtriomlem  10355  ltexprlem3  10951  nnunb  12398  indstr  12835  qbtwnxr  13120  qsqueeze  13121  xrsupsslem  13227  xrinfmsslem  13228  ioc0  13313  climshftlem  15499  o1rlimmul  15544  ramub2  16944  monmat2matmon  22727  tgcl  22872  neips  23016  ssnei2  23019  tgcnp  23156  cnpnei  23167  cnpco  23170  hauscmplem  23309  hauscmp  23310  llyss  23382  nllyss  23383  lfinun  23428  kgen2ss  23458  txcnpi  23511  txcmplem1  23544  fgss  23776  cnpflf2  23903  fclsss1  23925  fclscf  23928  alexsubALT  23954  cnextcn  23970  tsmsxp  24058  mopni3  24398  psmetutop  24471  tngngp3  24560  iscau4  25195  caussi  25213  ovolgelb  25397  mbfi1flim  25640  ellimc3  25796  lhop1  25935  tgbtwndiff  28469  axcontlem4  28930  clwwlknonwwlknonb  30068  sspmval  30695  shmodsi  31351  atcvat4i  32359  cdj3lem2b  32399  ifeqeqx  32504  acunirnmpt  32616  xrge0infss  32716  constrextdg2lem  33714  crefss  33815  issgon  34089  cvmlift2lem12  35286  satfv1  35335  satfvsucsuc  35337  ss2mcls  35540  btwndiff  36000  seglecgr12im  36083  fnessref  36330  waj-ax  36387  lukshef-ax2  36388  bj-isrvec  37267  icorempo  37324  finxpreclem1  37362  fvineqsneq  37385  pibt2  37390  tan2h  37591  poimirlem31  37630  poimir  37632  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  cvrat4  39422  athgt  39435  ps-2  39457  paddss1  39796  paddss2  39797  cdlemg33b0  40680  cdlemg33a  40685  dihjat1lem  41407  fphpdo  42790  irrapxlem2  42796  pell14qrss1234  42829  pell1qrss14  42841  acongtr  42951  ofoaid1  43331  ofoaid2  43332  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  grumnudlem  44258  ax6e2eq  44531  modelaxreplem1  44952  islptre  45601  limccog  45602  grilcbri2  47987  opnneilv  48881