Theorem anim2d 611

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 608	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 206  df-an 396

This theorem is referenced by:  darii  2666  festino  2675  baroco  2677  moeq3  3642  sbcimdv  3786  ssel  3910  sselOLD  3911  sscon  4069  uniss  4844  trel3  5195  ssopab2  5452  coss1  5753  fununi  6493  imadif  6502  fss  6601  ssimaex  6835  ssoprab2  7321  poxp  7940  soxp  7941  suppofssd  7990  pmss12g  8615  ss2ixp  8656  xpdom2  8807  fisup2g  9157  fisupcl  9158  fiinf2g  9189  inf3lem1  9316  epfrs  9420  cfub  9936  cflm  9937  fin23lem34  10033  isf32lem2  10041  axcc4  10126  domtriomlem  10129  ltexprlem3  10725  nnunb  12159  indstr  12585  qbtwnxr  12863  qsqueeze  12864  xrsupsslem  12970  xrinfmsslem  12971  ioc0  13055  climshftlem  15211  o1rlimmul  15256  ramub2  16643  monmat2matmon  21881  tgcl  22027  neips  22172  ssnei2  22175  tgcnp  22312  cnpnei  22323  cnpco  22326  hauscmplem  22465  hauscmp  22466  llyss  22538  nllyss  22539  lfinun  22584  kgen2ss  22614  txcnpi  22667  txcmplem1  22700  fgss  22932  cnpflf2  23059  fclsss1  23081  fclscf  23084  alexsubALT  23110  cnextcn  23126  tsmsxp  23214  mopni3  23556  psmetutop  23629  tngngp3  23726  iscau4  24348  caussi  24366  ovolgelb  24549  mbfi1flim  24793  ellimc3  24948  lhop1  25083  tgbtwndiff  26771  axcontlem4  27238  clwwlknonwwlknonb  28371  sspmval  28996  shmodsi  29652  atcvat4i  30660  cdj3lem2b  30700  ifeqeqx  30786  acunirnmpt  30898  xrge0infss  30985  crefss  31701  issgon  31991  cvmlift2lem12  33176  satfv1  33225  satfvsucsuc  33227  ss2mcls  33430  poseq  33729  btwndiff  34256  seglecgr12im  34339  fnessref  34473  waj-ax  34530  lukshef-ax2  34531  bj-isrvec  35392  icorempo  35449  finxpreclem1  35487  fvineqsneq  35510  pibt2  35515  tan2h  35696  poimirlem31  35735  poimir  35737  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  cvrat4  37384  athgt  37397  ps-2  37419  paddss1  37758  paddss2  37759  cdlemg33b0  38642  cdlemg33a  38647  dihjat1lem  39369  fphpdo  40555  irrapxlem2  40561  pell14qrss1234  40594  pell1qrss14  40606  acongtr  40716  grumnudlem  41792  ax6e2eq  42066  islptre  43050  limccog  43051  opnneilv  46090