Theorem anim2d 618

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  darii  2669  festino  2678  baroco  2680  moeq3  3660  sbcimdv  3798  ssel  3916  sscon  4080  uniss  4853  trel3  5195  axprlem4  5362  ssopab2  5495  coss1  5804  fununi  6567  imadif  6576  fss  6678  ssimaex  6919  ssoprab2  7431  poxp  8075  soxp  8076  poseq  8105  suppofssd  8150  pmss12g  8814  ss2ixp  8855  xpdom2  9007  fisup2g  9379  fisupcl  9380  fiinf2g  9412  elirrvOLD  9510  inf3lem1  9547  epfrs  9650  cfub  10169  cflm  10170  fin23lem34  10266  isf32lem2  10274  axcc4  10359  domtriomlem  10362  ltexprlem3  10959  nnunb  12431  indstr  12864  qbtwnxr  13150  qsqueeze  13151  xrsupsslem  13257  xrinfmsslem  13258  ioc0  13343  climshftlem  15534  o1rlimmul  15579  ramub2  16983  chnrss  18579  monmat2matmon  22814  tgcl  22959  neips  23103  ssnei2  23106  tgcnp  23243  cnpnei  23254  cnpco  23257  hauscmplem  23396  hauscmp  23397  llyss  23469  nllyss  23470  lfinun  23515  kgen2ss  23545  txcnpi  23598  txcmplem1  23631  fgss  23863  cnpflf2  23990  fclsss1  24012  fclscf  24015  alexsubALT  24041  cnextcn  24057  tsmsxp  24145  mopni3  24484  psmetutop  24557  tngngp3  24646  iscau4  25271  caussi  25289  ovolgelb  25472  mbfi1flim  25715  ellimc3  25871  lhop1  26006  tgbtwndiff  28599  axcontlem4  29061  clwwlknonwwlknonb  30201  sspmval  30829  shmodsi  31485  atcvat4i  32493  cdj3lem2b  32533  ifeqeqx  32637  acunirnmpt  32758  xrge0infss  32859  constrextdg2lem  33939  crefss  34040  issgon  34314  r1omhfb  35303  r1omhfbregs  35328  cvmlift2lem12  35543  satfv1  35592  satfvsucsuc  35594  ss2mcls  35797  btwndiff  36256  seglecgr12im  36339  fnessref  36586  waj-ax  36643  lukshef-ax2  36644  bj-isrvec  37655  icorempo  37714  finxpreclem1  37752  fvineqsneq  37775  pibt2  37780  wl-dfcleq  37877  tan2h  37980  poimirlem31  38019  poimir  38021  mblfinlem3  38027  mblfinlem4  38028  ismblfin  38029  cvrat4  39936  athgt  39949  ps-2  39971  paddss1  40310  paddss2  40311  cdlemg33b0  41194  cdlemg33a  41199  dihjat1lem  41921  fphpdo  43263  irrapxlem2  43269  pell14qrss1234  43302  pell1qrss14  43314  acongtr  43424  ofoaid1  43804  ofoaid2  43805  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  grumnudlem  44730  ax6e2eq  45002  modelaxreplem1  45423  islptre  46065  limccog  46066  grilcbri2  48503  opnneilv  49400