MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61d Structured version   Visualization version   GIF version

Theorem pm2.61d 171
Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
Hypotheses
Ref Expression
pm2.61d.1 (𝜑 → (𝜓𝜒))
pm2.61d.2 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
pm2.61d (𝜑𝜒)

Proof of Theorem pm2.61d
StepHypRef Expression
1 pm2.61d.2 . . . 4 (𝜑 → (¬ 𝜓𝜒))
21con1d 141 . . 3 (𝜑 → (¬ 𝜒𝜓))
3 pm2.61d.1 . . 3 (𝜑 → (𝜓𝜒))
42, 3syld 47 . 2 (𝜑 → (¬ 𝜒𝜒))
54pm2.18d 125 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61d1  172  pm2.61d2  173  pm5.21ndd  368  bija  369  pm2.61dan  796  ecase3d  1019  pm2.61dne  3028  ordunidif  5916  dff3  6515  tfindsg  7206  findsg  7239  brtpos  7512  omwordi  7804  omass  7813  nnmwordi  7868  pssnn  8333  frfi  8360  ixpiunwdom  8651  cantnfp1lem3  8740  infxpenlem  9035  infxp  9238  ackbij1lem16  9258  axpowndlem3  9622  pwfseqlem4a  9684  gchina  9722  prlem936  10070  supsrlem  10133  flflp1  12815  hashunx  13376  swrdccat3blem  13703  repswswrd  13739  sumss  14662  fsumss  14663  prodss  14883  fprodss  14884  ruclem2  15166  prmind2  15604  rpexp  15638  fermltl  15695  prmreclem5  15830  ramcl  15939  wunress  16147  divsfval  16414  efgsfo  18358  lt6abl  18502  gsumval3  18514  mdetunilem8  20642  ordtrest2lem  21227  ptpjpre1  21594  fbfinnfr  21864  filufint  21943  ptcmplem2  22076  cphsqrtcl3  23205  ovoliun  23492  voliunlem3  23539  volsup  23543  cxpsqrt  24669  amgm  24937  wilthlem2  25015  sqff1o  25128  chtublem  25156  bposlem1  25229  bposlem3  25231  ostth  25548  clwwisshclwwslemlem  27160  atdmd  29591  atmd2  29593  mdsymlem4  29599  ordtrest2NEWlem  30302  eulerpartlemb  30764  dfon2lem9  32026  nosupbnd1lem1  32185  nn0prpwlem  32648  ltflcei  33723  poimirlem30  33765  lplnexllnN  35365  2llnjaN  35367  paddasslem14  35634  cdleme32le  36249  dgrsub2  38224  iccelpart  41887  lighneallem3  42042  lighneal  42046
  Copyright terms: Public domain W3C validator