Theorem anim2d 612

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 609	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 207  df-an 396

This theorem is referenced by:  darii  2662  festino  2671  baroco  2673  moeq3  3668  sbcimdv  3807  ssel  3925  sscon  4094  uniss  4868  trel3  5211  axprlem4  5368  ssopab2  5491  coss1  5802  fununi  6564  imadif  6573  fss  6675  ssimaex  6916  ssoprab2  7423  poxp  8067  soxp  8068  poseq  8097  suppofssd  8142  pmss12g  8802  ss2ixp  8843  xpdom2  8995  fisup2g  9363  fisupcl  9364  fiinf2g  9396  elirrv  9493  inf3lem1  9528  epfrs  9631  cfub  10150  cflm  10151  fin23lem34  10247  isf32lem2  10255  axcc4  10340  domtriomlem  10343  ltexprlem3  10939  nnunb  12387  indstr  12824  qbtwnxr  13109  qsqueeze  13110  xrsupsslem  13216  xrinfmsslem  13217  ioc0  13302  climshftlem  15491  o1rlimmul  15536  ramub2  16936  chnrss  18531  monmat2matmon  22749  tgcl  22894  neips  23038  ssnei2  23041  tgcnp  23178  cnpnei  23189  cnpco  23192  hauscmplem  23331  hauscmp  23332  llyss  23404  nllyss  23405  lfinun  23450  kgen2ss  23480  txcnpi  23533  txcmplem1  23566  fgss  23798  cnpflf2  23925  fclsss1  23947  fclscf  23950  alexsubALT  23976  cnextcn  23992  tsmsxp  24080  mopni3  24419  psmetutop  24492  tngngp3  24581  iscau4  25216  caussi  25234  ovolgelb  25418  mbfi1flim  25661  ellimc3  25817  lhop1  25956  tgbtwndiff  28494  axcontlem4  28956  clwwlknonwwlknonb  30097  sspmval  30724  shmodsi  31380  atcvat4i  32388  cdj3lem2b  32428  ifeqeqx  32533  acunirnmpt  32652  xrge0infss  32754  constrextdg2lem  33772  crefss  33873  issgon  34147  r1omhfb  35134  r1omhfbregs  35144  cvmlift2lem12  35369  satfv1  35418  satfvsucsuc  35420  ss2mcls  35623  btwndiff  36082  seglecgr12im  36165  fnessref  36412  waj-ax  36469  lukshef-ax2  36470  bj-isrvec  37349  icorempo  37406  finxpreclem1  37444  fvineqsneq  37467  pibt2  37472  tan2h  37662  poimirlem31  37701  poimir  37703  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  cvrat4  39552  athgt  39565  ps-2  39587  paddss1  39926  paddss2  39927  cdlemg33b0  40810  cdlemg33a  40815  dihjat1lem  41537  fphpdo  42924  irrapxlem2  42930  pell14qrss1234  42963  pell1qrss14  42975  acongtr  43085  ofoaid1  43465  ofoaid2  43466  fzunt  43562  fzuntd  43563  fzunt1d  43564  fzuntgd  43565  grumnudlem  44392  ax6e2eq  44664  modelaxreplem1  45085  islptre  45733  limccog  45734  grilcbri2  48125  opnneilv  49023