Theorem anim2d 613

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  darii  2665  festino  2674  baroco  2676  moeq3  3661  sbcimdv  3804  ssel  3928  sselOLD  3929  sscon  4089  uniss  4864  trel3  5223  ssopab2  5494  coss1  5801  fununi  6563  imadif  6572  fss  6672  ssimaex  6913  ssoprab2  7409  poxp  8040  soxp  8041  poseq  8049  suppofssd  8093  pmss12g  8732  ss2ixp  8773  xpdom2  8936  fisup2g  9329  fisupcl  9330  fiinf2g  9361  inf3lem1  9489  epfrs  9592  cfub  10110  cflm  10111  fin23lem34  10207  isf32lem2  10215  axcc4  10300  domtriomlem  10303  ltexprlem3  10899  nnunb  12334  indstr  12761  qbtwnxr  13039  qsqueeze  13040  xrsupsslem  13146  xrinfmsslem  13147  ioc0  13231  climshftlem  15382  o1rlimmul  15427  ramub2  16812  monmat2matmon  22078  tgcl  22224  neips  22369  ssnei2  22372  tgcnp  22509  cnpnei  22520  cnpco  22523  hauscmplem  22662  hauscmp  22663  llyss  22735  nllyss  22736  lfinun  22781  kgen2ss  22811  txcnpi  22864  txcmplem1  22897  fgss  23129  cnpflf2  23256  fclsss1  23278  fclscf  23281  alexsubALT  23307  cnextcn  23323  tsmsxp  23411  mopni3  23755  psmetutop  23828  tngngp3  23925  iscau4  24548  caussi  24566  ovolgelb  24749  mbfi1flim  24993  ellimc3  25148  lhop1  25283  tgbtwndiff  27155  axcontlem4  27623  clwwlknonwwlknonb  28757  sspmval  29382  shmodsi  30038  atcvat4i  31046  cdj3lem2b  31086  ifeqeqx  31170  acunirnmpt  31281  xrge0infss  31368  crefss  32095  issgon  32387  cvmlift2lem12  33573  satfv1  33622  satfvsucsuc  33624  ss2mcls  33827  btwndiff  34466  seglecgr12im  34549  fnessref  34683  waj-ax  34740  lukshef-ax2  34741  bj-isrvec  35619  icorempo  35676  finxpreclem1  35714  fvineqsneq  35737  pibt2  35742  tan2h  35925  poimirlem31  35964  poimir  35966  mblfinlem3  35972  mblfinlem4  35973  ismblfin  35974  cvrat4  37762  athgt  37775  ps-2  37797  paddss1  38136  paddss2  38137  cdlemg33b0  39020  cdlemg33a  39025  dihjat1lem  39747  fphpdo  40952  irrapxlem2  40958  pell14qrss1234  40991  pell1qrss14  41003  acongtr  41114  ofoaid1  41376  ofoaid2  41377  fzunt  41436  fzuntd  41437  fzunt1d  41438  fzuntgd  41439  grumnudlem  42276  ax6e2eq  42550  islptre  43548  limccog  43549  opnneilv  46620