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  3671  sbcimdv  3810  ssel  3928  sscon  4096  uniss  4872  trel3  5215  axprlem4  5372  ssopab2  5495  coss1  5805  fununi  6568  imadif  6577  fss  6679  ssimaex  6920  ssoprab2  7428  poxp  8072  soxp  8073  poseq  8102  suppofssd  8147  pmss12g  8811  ss2ixp  8852  xpdom2  9004  fisup2g  9376  fisupcl  9377  fiinf2g  9409  elirrv  9506  inf3lem1  9541  epfrs  9644  cfub  10163  cflm  10164  fin23lem34  10260  isf32lem2  10268  axcc4  10353  domtriomlem  10356  ltexprlem3  10953  nnunb  12401  indstr  12833  qbtwnxr  13119  qsqueeze  13120  xrsupsslem  13226  xrinfmsslem  13227  ioc0  13312  climshftlem  15501  o1rlimmul  15546  ramub2  16946  chnrss  18542  monmat2matmon  22772  tgcl  22917  neips  23061  ssnei2  23064  tgcnp  23201  cnpnei  23212  cnpco  23215  hauscmplem  23354  hauscmp  23355  llyss  23427  nllyss  23428  lfinun  23473  kgen2ss  23503  txcnpi  23556  txcmplem1  23589  fgss  23821  cnpflf2  23948  fclsss1  23970  fclscf  23973  alexsubALT  23999  cnextcn  24015  tsmsxp  24103  mopni3  24442  psmetutop  24515  tngngp3  24604  iscau4  25239  caussi  25257  ovolgelb  25441  mbfi1flim  25684  ellimc3  25840  lhop1  25979  tgbtwndiff  28561  axcontlem4  29023  clwwlknonwwlknonb  30164  sspmval  30791  shmodsi  31447  atcvat4i  32455  cdj3lem2b  32495  ifeqeqx  32599  acunirnmpt  32719  xrge0infss  32821  constrextdg2lem  33886  crefss  33987  issgon  34261  r1omhfb  35249  r1omhfbregs  35274  cvmlift2lem12  35489  satfv1  35538  satfvsucsuc  35540  ss2mcls  35743  btwndiff  36202  seglecgr12im  36285  fnessref  36532  waj-ax  36589  lukshef-ax2  36590  bj-isrvec  37470  icorempo  37527  finxpreclem1  37565  fvineqsneq  37588  pibt2  37593  tan2h  37784  poimirlem31  37823  poimir  37825  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  cvrat4  39740  athgt  39753  ps-2  39775  paddss1  40114  paddss2  40115  cdlemg33b0  40998  cdlemg33a  41003  dihjat1lem  41725  fphpdo  43095  irrapxlem2  43101  pell14qrss1234  43134  pell1qrss14  43146  acongtr  43256  ofoaid1  43636  ofoaid2  43637  fzunt  43732  fzuntd  43733  fzunt1d  43734  fzuntgd  43735  grumnudlem  44562  ax6e2eq  44834  modelaxreplem1  45255  islptre  45901  limccog  45902  grilcbri2  48293  opnneilv  49190