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  2694  festino  2703  baroco  2705  moeq3  3678  sbcimdv  3815  ssel  3933  sscon  4099  uniss  4876  trel3  5221  axprlem4  5388  ssopab2  5522  coss1  5832  fununi  6600  imadif  6609  fss  6712  ssimaex  6956  ssoprab2  7468  poxp  8112  soxp  8113  poseq  8142  suppofssd  8187  pmss12g  8855  ss2ixp  8896  xpdom2  9048  fisup2g  9417  fisupcl  9418  fiinf2g  9450  elirrvOLD  9548  inf3lem1  9585  epfrs  9688  cfub  10220  cflm  10221  fin23lem34  10318  isf32lem2  10326  axcc4  10411  domtriomlem  10414  ltexprlem3  11011  nnunb  12491  indstr  12931  qbtwnxr  13217  qsqueeze  13218  xrsupsslem  13324  xrinfmsslem  13325  ioc0  13410  climshftlem  15615  o1rlimmul  15660  ramub2  17064  chnrss  18661  monmat2matmon  22942  tgcl  23087  neips  23231  ssnei2  23234  tgcnp  23371  cnpnei  23382  cnpco  23385  hauscmplem  23524  hauscmp  23525  llyss  23597  nllyss  23598  lfinun  23643  kgen2ss  23673  txcnpi  23726  txcmplem1  23759  fgss  23991  cnpflf2  24118  fclsss1  24140  fclscf  24143  alexsubALT  24169  cnextcn  24185  tsmsxp  24273  mopni3  24612  psmetutop  24685  tngngp3  24774  iscau4  25399  caussi  25417  ovolgelb  25600  mbfi1flim  25843  ellimc3  25999  lhop1  26134  tgbtwndiff  28733  axcontlem4  29226  clwwlknonwwlknonb  30366  sspmval  30994  shmodsi  31650  atcvat4i  32658  cdj3lem2b  32698  ifeqeqx  32798  acunirnmpt  32916  xrge0infss  33017  constrextdg2lem  34055  crefss  34156  issgon  34430  r1omhfb  35420  r1omhfbregs  35445  cvmlift2lem12  35677  satfv1  35726  satfvsucsuc  35728  ss2mcls  35931  btwndiff  36390  seglecgr12im  36473  fnessref  36730  waj-ax  36787  lukshef-ax2  36788  bj-isrvec  37798  icorempo  37857  finxpreclem1  37895  fvineqsneq  37918  pibt2  37923  wl-dfcleq  38020  tan2h  38123  poimirlem31  38162  poimir  38164  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  cvrat4  40079  athgt  40092  ps-2  40114  paddss1  40453  paddss2  40454  cdlemg33b0  41337  cdlemg33a  41342  dihjat1lem  42064  fphpdo  43406  irrapxlem2  43412  pell14qrss1234  43445  pell1qrss14  43457  acongtr  43567  ofoaid1  43947  ofoaid2  43948  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  grumnudlem  44859  ax6e2eq  45131  modelaxreplem1  45552  islptre  46193  limccog  46194  grilcbri2  48631  opnneilv  49538