Theorem anim2d 624

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  darii  2691  festino  2700  baroco  2702  moeq3  3673  sbcimdv  3810  ssel  3928  sscon  4093  uniss  4878  trel3  5225  axprlem4  5395  ssopab2  5529  coss1  5839  fununi  6612  imadif  6621  fss  6723  ssimaex  6967  ssoprab2  7484  poxp  8129  soxp  8130  poseq  8159  suppofssd  8204  pmss12g  8879  ss2ixp  8920  xpdom2  9073  fisup2g  9442  fisupcl  9443  fiinf2g  9475  elirrvOLD  9573  inf3lem1  9610  epfrs  9713  cfub  10253  cflm  10254  fin23lem34  10351  isf32lem2  10359  axcc4  10444  domtriomlem  10447  ltexprlem3  11050  nnunb  12527  indstr  12968  qbtwnxr  13254  qsqueeze  13255  xrsupsslem  13361  xrinfmsslem  13362  ioc0  13447  climshftlem  15663  o1rlimmul  15708  ramub2  17110  chnrss  18707  monmat2matmon  23053  tgcl  23198  neips  23342  ssnei2  23345  tgcnp  23482  cnpnei  23493  cnpco  23496  hauscmplem  23635  hauscmp  23636  llyss  23709  nllyss  23710  lfinun  23755  kgen2ss  23785  txcnpi  23838  txcmplem1  23871  fgss  24103  cnpflf2  24230  fclsss1  24252  fclscf  24255  alexsubALT  24281  cnextcn  24297  tsmsxp  24385  mopni3  24724  psmetutop  24797  tngngp3  24886  iscau4  25511  caussi  25529  ovolgelb  25712  mbfi1flim  25955  ellimc3  26111  lhop1  26246  tgbtwndiff  28849  axcontlem4  29425  clwwlknonwwlknonb  30577  sspmval  31215  shmodsi  31871  atcvat4i  32879  cdj3lem2b  32919  ifeqeqx  33018  acunirnmpt  33134  xrge0infss  33233  constrextdg2lem  34260  crefss  34361  issgon  34635  r1omhfb  35624  r1omhfbregs  35665  cvmlift2lem12  35895  satfv1  35944  satfvsucsuc  35946  ss2mcls  36149  btwndiff  36609  seglecgr12im  36692  fnessref  36978  waj-ax  37035  lukshef-ax2  37036  bj-isrvec  38048  icorempo  38107  finxpreclem1  38145  fvineqsneq  38168  pibt2  38173  wl-dfcleq  38270  tan2h  38368  poimirlem31  38402  poimir  38404  mblfinlem3  38410  mblfinlem4  38411  ismblfin  38412  cvrat4  40318  athgt  40331  ps-2  40353  paddss1  40692  paddss2  40693  cdlemg33b0  41576  cdlemg33a  41581  dihjat1lem  42303  fphpdo  43660  irrapxlem2  43666  pell14qrss1234  43699  pell1qrss14  43711  acongtr  43821  ofoaid1  44201  ofoaid2  44202  fzunt  44297  fzuntd  44298  fzunt1d  44299  fzuntgd  44300  grumnudlem  45111  ax6e2eq  45382  modelaxreplem1  45803  islptre  46451  limccog  46452  grilcbri2  48929  opnneilv  49837