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 398

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 209  df-an 399

This theorem is referenced by:  sbimdvOLD  2512  sbimdOLD  2514  darii  2748  festino  2757  baroco  2759  moeq3  3703  ssel  3961  sscon  4115  uniss  4853  trel3  5173  ssopab2  5426  coss1  5721  fununi  6424  imadif  6433  fss  6522  ssimaex  6743  ssoprab2  7216  poxp  7816  soxp  7817  suppofssd  7861  pmss12g  8427  ss2ixp  8468  xpdom2  8606  fisup2g  8926  fisupcl  8927  fiinf2g  8958  inf3lem1  9085  epfrs  9167  cfub  9665  cflm  9666  fin23lem34  9762  isf32lem2  9770  axcc4  9855  domtriomlem  9858  ltexprlem3  10454  nnunb  11887  indstr  12310  qbtwnxr  12587  qsqueeze  12588  xrsupsslem  12694  xrinfmsslem  12695  ioc0  12779  climshftlem  14925  o1rlimmul  14969  ramub2  16344  monmat2matmon  21426  tgcl  21571  neips  21715  ssnei2  21718  tgcnp  21855  cnpnei  21866  cnpco  21869  hauscmplem  22008  hauscmp  22009  llyss  22081  nllyss  22082  lfinun  22127  kgen2ss  22157  txcnpi  22210  txcmplem1  22243  fgss  22475  cnpflf2  22602  fclsss1  22624  fclscf  22627  alexsubALT  22653  cnextcn  22669  tsmsxp  22757  mopni3  23098  psmetutop  23171  tngngp3  23259  iscau4  23876  caussi  23894  ovolgelb  24075  mbfi1flim  24318  ellimc3  24471  lhop1  24605  tgbtwndiff  26286  axcontlem4  26747  clwwlknonwwlknonb  27879  sspmval  28504  shmodsi  29160  atcvat4i  30168  cdj3lem2b  30208  ifeqeqx  30291  acunirnmpt  30398  xrge0infss  30478  crefss  31108  issgon  31377  cvmlift2lem12  32556  satfv1  32605  satfvsucsuc  32607  ss2mcls  32810  poseq  33090  btwndiff  33483  seglecgr12im  33566  fnessref  33700  waj-ax  33757  lukshef-ax2  33758  icorempo  34626  finxpreclem1  34664  fvineqsneq  34687  pibt2  34692  tan2h  34878  poimirlem31  34917  poimir  34919  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  cvrat4  36573  athgt  36586  ps-2  36608  paddss1  36947  paddss2  36948  cdlemg33b0  37831  cdlemg33a  37836  dihjat1lem  38558  fphpdo  39407  irrapxlem2  39413  pell14qrss1234  39446  pell1qrss14  39458  acongtr  39568  grumnudlem  40614  ax6e2eq  40884  islptre  41892  limccog  41893