Theorem anim2d 624

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  darii  2692  festino  2701  baroco  2703  moeq3  3673  sbcimdv  3810  ssel  3907  sscon  4082  uniss  4878  trel3  5224  axprlem4  5392  ssopab2  5525  coss1  5839  fununi  6637  imadif  6646  fss  6748  ssimaex  6993  ssoprab2  7511  poxp  8167  soxp  8168  poseq  8202  suppofssd  8248  pmss12g  8925  ss2ixp  8966  xpdom2  9119  fisup2g  9488  fisupcl  9489  fiinf2g  9521  elirrvOLD  9619  inf3lem1  9656  epfrs  9759  cfub  10353  cflm  10354  fin23lem34  10451  isf32lem2  10459  axcc4  10544  domtriomlem  10547  ltexprlem3  11150  nnunb  12629  indstr  13070  qbtwnxr  13357  qsqueeze  13358  xrsupsslem  13464  xrinfmsslem  13465  ioc0  13550  climshftlem  15770  o1rlimmul  15815  ramub2  17221  chnrss  18818  monmat2matmon  23172  tgcl  23317  neips  23461  ssnei2  23464  tgcnp  23601  cnpnei  23612  cnpco  23615  hauscmplem  23754  hauscmp  23755  llyss  23828  nllyss  23829  lfinun  23874  kgen2ss  23904  txcnpi  23957  txcmplem1  23990  fgss  24222  cnpflf2  24349  fclsss1  24371  fclscf  24374  alexsubALT  24400  cnextcn  24416  tsmsxp  24504  mopni3  24843  psmetutop  24916  tngngp3  25005  iscau4  25630  caussi  25648  ovolgelb  25831  mbfi1flim  26074  ellimc3  26229  lhop1  26364  tgbtwndiff  28999  axcontlem4  29575  clwwlknonwwlknonb  30727  sspmval  31365  shmodsi  32021  atcvat4i  33029  cdj3lem2b  33069  ifeqeqx  33210  acunirnmpt  33325  xrge0infss  33422  constrextdg2lem  34450  crefss  34551  issgon  34825  eqhf  35820  eqhfregs  35905  cvmlift2lem12  36246  satfv1  36295  satfvsucsuc  36297  ss2mcls  36500  btwndiff  36970  seglecgr12im  37053  fnessref  37323  waj-ax  37380  lukshef-ax2  37381  bj-isrvec  38407  icorempo  38466  finxpreclem1  38504  fvineqsneq  38527  pibt2  38532  wl-dfcleq  38629  tan2h  38727  poimirlem31  38761  poimir  38763  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  cvrat4  40692  athgt  40705  ps-2  40727  paddss1  41066  paddss2  41067  cdlemg33b0  41950  cdlemg33a  41955  dihjat1lem  42677  fphpdo  44017  irrapxlem2  44023  pell14qrss1234  44056  pell1qrss14  44068  acongtr  44178  ofoaid1  44552  ofoaid2  44553  fzunt  44648  fzuntd  44649  fzunt1d  44650  fzuntgd  44651  grumnudlem  45461  ax6e2eq  45731  modelaxreplem1  46163  islptre  46836  limccog  46837  grilcbri2  49314  opnneilv  50228