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  3683  sbcimdv  3822  ssel  3940  sscon  4106  uniss  4879  trel3  5224  axprlem4  5381  ssopab2  5506  coss1  5819  fununi  6591  imadif  6600  fss  6704  ssimaex  6946  ssoprab2  7457  poxp  8107  soxp  8108  poseq  8137  suppofssd  8182  pmss12g  8842  ss2ixp  8883  xpdom2  9036  fisup2g  9420  fisupcl  9421  fiinf2g  9453  inf3lem1  9581  epfrs  9684  cfub  10202  cflm  10203  fin23lem34  10299  isf32lem2  10307  axcc4  10392  domtriomlem  10395  ltexprlem3  10991  nnunb  12438  indstr  12875  qbtwnxr  13160  qsqueeze  13161  xrsupsslem  13267  xrinfmsslem  13268  ioc0  13353  climshftlem  15540  o1rlimmul  15585  ramub2  16985  monmat2matmon  22711  tgcl  22856  neips  23000  ssnei2  23003  tgcnp  23140  cnpnei  23151  cnpco  23154  hauscmplem  23293  hauscmp  23294  llyss  23366  nllyss  23367  lfinun  23412  kgen2ss  23442  txcnpi  23495  txcmplem1  23528  fgss  23760  cnpflf2  23887  fclsss1  23909  fclscf  23912  alexsubALT  23938  cnextcn  23954  tsmsxp  24042  mopni3  24382  psmetutop  24455  tngngp3  24544  iscau4  25179  caussi  25197  ovolgelb  25381  mbfi1flim  25624  ellimc3  25780  lhop1  25919  tgbtwndiff  28433  axcontlem4  28894  clwwlknonwwlknonb  30035  sspmval  30662  shmodsi  31318  atcvat4i  32326  cdj3lem2b  32366  ifeqeqx  32471  acunirnmpt  32583  xrge0infss  32683  constrextdg2lem  33738  crefss  33839  issgon  34113  cvmlift2lem12  35301  satfv1  35350  satfvsucsuc  35352  ss2mcls  35555  btwndiff  36015  seglecgr12im  36098  fnessref  36345  waj-ax  36402  lukshef-ax2  36403  bj-isrvec  37282  icorempo  37339  finxpreclem1  37377  fvineqsneq  37400  pibt2  37405  tan2h  37606  poimirlem31  37645  poimir  37647  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  cvrat4  39437  athgt  39450  ps-2  39472  paddss1  39811  paddss2  39812  cdlemg33b0  40695  cdlemg33a  40700  dihjat1lem  41422  fphpdo  42805  irrapxlem2  42811  pell14qrss1234  42844  pell1qrss14  42856  acongtr  42967  ofoaid1  43347  ofoaid2  43348  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  grumnudlem  44274  ax6e2eq  44547  modelaxreplem1  44968  islptre  45617  limccog  45618  grilcbri2  48003  opnneilv  48897