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 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  2666  festino  2675  baroco  2677  moeq3  3659  sbcimdv  3798  ssel  3916  sscon  4084  uniss  4859  trel3  5202  axprlem4  5361  ssopab2  5492  coss1  5802  fununi  6565  imadif  6574  fss  6676  ssimaex  6917  ssoprab2  7426  poxp  8069  soxp  8070  poseq  8099  suppofssd  8144  pmss12g  8808  ss2ixp  8849  xpdom2  9001  fisup2g  9373  fisupcl  9374  fiinf2g  9406  elirrv  9503  inf3lem1  9538  epfrs  9641  cfub  10160  cflm  10161  fin23lem34  10257  isf32lem2  10265  axcc4  10350  domtriomlem  10353  ltexprlem3  10950  nnunb  12422  indstr  12855  qbtwnxr  13141  qsqueeze  13142  xrsupsslem  13248  xrinfmsslem  13249  ioc0  13334  climshftlem  15525  o1rlimmul  15570  ramub2  16974  chnrss  18570  monmat2matmon  22798  tgcl  22943  neips  23087  ssnei2  23090  tgcnp  23227  cnpnei  23238  cnpco  23241  hauscmplem  23380  hauscmp  23381  llyss  23453  nllyss  23454  lfinun  23499  kgen2ss  23529  txcnpi  23582  txcmplem1  23615  fgss  23847  cnpflf2  23974  fclsss1  23996  fclscf  23999  alexsubALT  24025  cnextcn  24041  tsmsxp  24129  mopni3  24468  psmetutop  24541  tngngp3  24630  iscau4  25255  caussi  25273  ovolgelb  25456  mbfi1flim  25699  ellimc3  25855  lhop1  25991  tgbtwndiff  28593  axcontlem4  29055  clwwlknonwwlknonb  30196  sspmval  30824  shmodsi  31480  atcvat4i  32488  cdj3lem2b  32528  ifeqeqx  32632  acunirnmpt  32752  xrge0infss  32853  constrextdg2lem  33913  crefss  34014  issgon  34288  r1omhfb  35277  r1omhfbregs  35302  cvmlift2lem12  35517  satfv1  35566  satfvsucsuc  35568  ss2mcls  35771  btwndiff  36230  seglecgr12im  36313  fnessref  36560  waj-ax  36617  lukshef-ax2  36618  bj-isrvec  37621  icorempo  37678  finxpreclem1  37716  fvineqsneq  37739  pibt2  37744  wl-dfcleq  37841  tan2h  37944  poimirlem31  37983  poimir  37985  mblfinlem3  37991  mblfinlem4  37992  ismblfin  37993  cvrat4  39900  athgt  39913  ps-2  39935  paddss1  40274  paddss2  40275  cdlemg33b0  41158  cdlemg33a  41163  dihjat1lem  41885  fphpdo  43260  irrapxlem2  43266  pell14qrss1234  43299  pell1qrss14  43311  acongtr  43421  ofoaid1  43801  ofoaid2  43802  fzunt  43897  fzuntd  43898  fzunt1d  43899  fzuntgd  43900  grumnudlem  44727  ax6e2eq  44999  modelaxreplem1  45420  islptre  46064  limccog  46065  grilcbri2  48484  opnneilv  49381