Theorem anim2d 614

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sbimdvOLD  2517  sbimdOLD  2519  darii  2750  festino  2759  baroco  2761  moeq3  3680  ssel  3937  sscon  4091  uniss  4819  trel3  5153  ssopab2  5406  coss1  5699  fununi  6402  imadif  6411  fss  6500  ssimaex  6721  ssoprab2  7196  poxp  7797  soxp  7798  suppofssd  7842  pmss12g  8408  ss2ixp  8449  xpdom2  8587  fisup2g  8908  fisupcl  8909  fiinf2g  8940  inf3lem1  9067  epfrs  9149  cfub  9648  cflm  9649  fin23lem34  9745  isf32lem2  9753  axcc4  9838  domtriomlem  9841  ltexprlem3  10437  nnunb  11871  indstr  12294  qbtwnxr  12571  qsqueeze  12572  xrsupsslem  12678  xrinfmsslem  12679  ioc0  12763  climshftlem  14910  o1rlimmul  14954  ramub2  16327  monmat2matmon  21407  tgcl  21552  neips  21696  ssnei2  21699  tgcnp  21836  cnpnei  21847  cnpco  21850  hauscmplem  21989  hauscmp  21990  llyss  22062  nllyss  22063  lfinun  22108  kgen2ss  22138  txcnpi  22191  txcmplem1  22224  fgss  22456  cnpflf2  22583  fclsss1  22605  fclscf  22608  alexsubALT  22634  cnextcn  22650  tsmsxp  22738  mopni3  23079  psmetutop  23152  tngngp3  23240  iscau4  23861  caussi  23879  ovolgelb  24062  mbfi1flim  24305  ellimc3  24460  lhop1  24595  tgbtwndiff  26278  axcontlem4  26739  clwwlknonwwlknonb  27869  sspmval  28494  shmodsi  29150  atcvat4i  30158  cdj3lem2b  30198  ifeqeqx  30283  acunirnmpt  30390  xrge0infss  30470  crefss  31123  issgon  31389  cvmlift2lem12  32568  satfv1  32617  satfvsucsuc  32619  ss2mcls  32822  poseq  33102  btwndiff  33495  seglecgr12im  33578  fnessref  33712  waj-ax  33769  lukshef-ax2  33770  icorempo  34648  finxpreclem1  34686  fvineqsneq  34709  pibt2  34714  tan2h  34927  poimirlem31  34966  poimir  34968  mblfinlem3  34974  mblfinlem4  34975  ismblfin  34976  cvrat4  36617  athgt  36630  ps-2  36652  paddss1  36991  paddss2  36992  cdlemg33b0  37875  cdlemg33a  37880  dihjat1lem  38602  fphpdo  39553  irrapxlem2  39559  pell14qrss1234  39592  pell1qrss14  39604  acongtr  39714  grumnudlem  40776  ax6e2eq  41046  islptre  42052  limccog  42053