Theorem anim2d 623

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 620	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  darii  2690  festino  2699  baroco  2701  moeq3  3674  sbcimdv  3811  ssel  3930  sscon  4096  uniss  4879  trel3  5226  axprlem4  5397  ssopab2  5531  coss1  5841  fununi  6611  imadif  6620  fss  6722  ssimaex  6966  ssoprab2  7478  poxp  8123  soxp  8124  poseq  8153  suppofssd  8198  pmss12g  8866  ss2ixp  8907  xpdom2  9059  fisup2g  9428  fisupcl  9429  fiinf2g  9461  elirrvOLD  9559  inf3lem1  9596  epfrs  9699  cfub  10231  cflm  10232  fin23lem34  10329  isf32lem2  10337  axcc4  10422  domtriomlem  10425  ltexprlem3  11022  nnunb  12499  indstr  12939  qbtwnxr  13225  qsqueeze  13226  xrsupsslem  13332  xrinfmsslem  13333  ioc0  13418  climshftlem  15625  o1rlimmul  15670  ramub2  17073  chnrss  18670  monmat2matmon  22960  tgcl  23105  neips  23249  ssnei2  23252  tgcnp  23389  cnpnei  23400  cnpco  23403  hauscmplem  23542  hauscmp  23543  llyss  23615  nllyss  23616  lfinun  23661  kgen2ss  23691  txcnpi  23744  txcmplem1  23777  fgss  24009  cnpflf2  24136  fclsss1  24158  fclscf  24161  alexsubALT  24187  cnextcn  24203  tsmsxp  24291  mopni3  24630  psmetutop  24703  tngngp3  24792  iscau4  25417  caussi  25435  ovolgelb  25618  mbfi1flim  25861  ellimc3  26017  lhop1  26152  tgbtwndiff  28751  axcontlem4  29283  clwwlknonwwlknonb  30423  sspmval  31051  shmodsi  31707  atcvat4i  32715  cdj3lem2b  32755  ifeqeqx  32854  acunirnmpt  32970  xrge0infss  33071  constrextdg2lem  34104  crefss  34205  issgon  34479  r1omhfb  35474  r1omhfbregs  35516  cvmlift2lem12  35772  satfv1  35821  satfvsucsuc  35823  ss2mcls  36026  btwndiff  36485  seglecgr12im  36568  fnessref  36834  waj-ax  36891  lukshef-ax2  36892  bj-isrvec  37904  icorempo  37963  finxpreclem1  38001  fvineqsneq  38024  pibt2  38029  wl-dfcleq  38126  tan2h  38229  poimirlem31  38268  poimir  38270  mblfinlem3  38276  mblfinlem4  38277  ismblfin  38278  cvrat4  40185  athgt  40198  ps-2  40220  paddss1  40559  paddss2  40560  cdlemg33b0  41443  cdlemg33a  41448  dihjat1lem  42170  fphpdo  43514  irrapxlem2  43520  pell14qrss1234  43553  pell1qrss14  43565  acongtr  43675  ofoaid1  44055  ofoaid2  44056  fzunt  44151  fzuntd  44152  fzunt1d  44153  fzuntgd  44154  grumnudlem  44965  ax6e2eq  45236  modelaxreplem1  45657  islptre  46305  limccog  46306  grilcbri2  48743  opnneilv  49654