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  5369  ssopab2  5501  coss1  5811  fununi  6574  imadif  6583  fss  6685  ssimaex  6926  ssoprab2  7435  poxp  8078  soxp  8079  poseq  8108  suppofssd  8153  pmss12g  8817  ss2ixp  8858  xpdom2  9010  fisup2g  9382  fisupcl  9383  fiinf2g  9415  elirrv  9512  inf3lem1  9549  epfrs  9652  cfub  10171  cflm  10172  fin23lem34  10268  isf32lem2  10276  axcc4  10361  domtriomlem  10364  ltexprlem3  10961  nnunb  12433  indstr  12866  qbtwnxr  13152  qsqueeze  13153  xrsupsslem  13259  xrinfmsslem  13260  ioc0  13345  climshftlem  15536  o1rlimmul  15581  ramub2  16985  chnrss  18581  monmat2matmon  22789  tgcl  22934  neips  23078  ssnei2  23081  tgcnp  23218  cnpnei  23229  cnpco  23232  hauscmplem  23371  hauscmp  23372  llyss  23444  nllyss  23445  lfinun  23490  kgen2ss  23520  txcnpi  23573  txcmplem1  23606  fgss  23838  cnpflf2  23965  fclsss1  23987  fclscf  23990  alexsubALT  24016  cnextcn  24032  tsmsxp  24120  mopni3  24459  psmetutop  24532  tngngp3  24621  iscau4  25246  caussi  25264  ovolgelb  25447  mbfi1flim  25690  ellimc3  25846  lhop1  25981  tgbtwndiff  28574  axcontlem4  29036  clwwlknonwwlknonb  30176  sspmval  30804  shmodsi  31460  atcvat4i  32468  cdj3lem2b  32508  ifeqeqx  32612  acunirnmpt  32732  xrge0infss  32833  constrextdg2lem  33892  crefss  33993  issgon  34267  r1omhfb  35256  r1omhfbregs  35281  cvmlift2lem12  35496  satfv1  35545  satfvsucsuc  35547  ss2mcls  35750  btwndiff  36209  seglecgr12im  36292  fnessref  36539  waj-ax  36596  lukshef-ax2  36597  bj-isrvec  37608  icorempo  37667  finxpreclem1  37705  fvineqsneq  37728  pibt2  37733  wl-dfcleq  37830  tan2h  37933  poimirlem31  37972  poimir  37974  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  cvrat4  39889  athgt  39902  ps-2  39924  paddss1  40263  paddss2  40264  cdlemg33b0  41147  cdlemg33a  41152  dihjat1lem  41874  fphpdo  43245  irrapxlem2  43251  pell14qrss1234  43284  pell1qrss14  43296  acongtr  43406  ofoaid1  43786  ofoaid2  43787  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  grumnudlem  44712  ax6e2eq  44984  modelaxreplem1  45405  islptre  46049  limccog  46050  grilcbri2  48481  opnneilv  49378