Theorem anim2d 620

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 617	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:  darii  2685  festino  2694  baroco  2696  moeq3  3669  sbcimdv  3807  ssel  3925  sscon  4091  uniss  4867  trel3  5210  axprlem4  5377  ssopab2  5510  coss1  5820  fununi  6585  imadif  6594  fss  6697  ssimaex  6941  ssoprab2  7453  poxp  8096  soxp  8097  poseq  8126  suppofssd  8171  pmss12g  8840  ss2ixp  8881  xpdom2  9033  fisup2g  9405  fisupcl  9406  fiinf2g  9438  elirrvOLD  9536  inf3lem1  9573  epfrs  9676  cfub  10195  cflm  10196  fin23lem34  10293  isf32lem2  10301  axcc4  10386  domtriomlem  10389  ltexprlem3  10986  nnunb  12467  indstr  12907  qbtwnxr  13193  qsqueeze  13194  xrsupsslem  13300  xrinfmsslem  13301  ioc0  13386  climshftlem  15577  o1rlimmul  15622  ramub2  17026  chnrss  18623  monmat2matmon  22857  tgcl  23002  neips  23146  ssnei2  23149  tgcnp  23286  cnpnei  23297  cnpco  23300  hauscmplem  23439  hauscmp  23440  llyss  23512  nllyss  23513  lfinun  23558  kgen2ss  23588  txcnpi  23641  txcmplem1  23674  fgss  23906  cnpflf2  24033  fclsss1  24055  fclscf  24058  alexsubALT  24084  cnextcn  24100  tsmsxp  24188  mopni3  24527  psmetutop  24600  tngngp3  24689  iscau4  25314  caussi  25332  ovolgelb  25515  mbfi1flim  25758  ellimc3  25914  lhop1  26049  tgbtwndiff  28645  axcontlem4  29107  clwwlknonwwlknonb  30247  sspmval  30875  shmodsi  31531  atcvat4i  32539  cdj3lem2b  32579  ifeqeqx  32683  acunirnmpt  32804  xrge0infss  32905  constrextdg2lem  33999  crefss  34100  issgon  34374  r1omhfb  35363  r1omhfbregs  35388  cvmlift2lem12  35612  satfv1  35661  satfvsucsuc  35663  ss2mcls  35866  btwndiff  36325  seglecgr12im  36408  fnessref  36665  waj-ax  36722  lukshef-ax2  36723  bj-isrvec  37734  icorempo  37793  finxpreclem1  37831  fvineqsneq  37854  pibt2  37859  wl-dfcleq  37956  tan2h  38059  poimirlem31  38098  poimir  38100  mblfinlem3  38106  mblfinlem4  38107  ismblfin  38108  cvrat4  40015  athgt  40028  ps-2  40050  paddss1  40389  paddss2  40390  cdlemg33b0  41273  cdlemg33a  41278  dihjat1lem  42000  fphpdo  43342  irrapxlem2  43348  pell14qrss1234  43381  pell1qrss14  43393  acongtr  43503  ofoaid1  43883  ofoaid2  43884  fzunt  43979  fzuntd  43980  fzunt1d  43981  fzuntgd  43982  grumnudlem  44809  ax6e2eq  45081  modelaxreplem1  45502  islptre  46143  limccog  46144  grilcbri2  48581  opnneilv  49478