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 170
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 139 . . 3 (𝜑 → (¬ 𝜒𝜓))
3 pm2.61d.1 . . 3 (𝜑 → (𝜓𝜒))
42, 3syld 47 . 2 (𝜑 → (¬ 𝜒𝜒))
54pm2.18d 124 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  171  pm2.61d2  172  pm5.21ndd  368  bija  369  pm2.61dan  867  ecase3d  1021  pm2.61dne  3018  ordunidif  5934  dff3  6536  tfindsg  7226  findsg  7259  brtpos  7531  omwordi  7822  omass  7831  nnmwordi  7886  pssnn  8345  frfi  8372  ixpiunwdom  8663  cantnfp1lem3  8752  infxpenlem  9046  infxp  9249  ackbij1lem16  9269  axpowndlem3  9633  pwfseqlem4a  9695  gchina  9733  prlem936  10081  supsrlem  10144  flflp1  12822  hashunx  13387  swrdccat3blem  13715  repswswrd  13751  sumss  14674  fsumss  14675  prodss  14896  fprodss  14897  ruclem2  15180  prmind2  15620  rpexp  15654  fermltl  15711  prmreclem5  15846  ramcl  15955  wunress  16162  divsfval  16429  efgsfo  18372  lt6abl  18516  gsumval3  18528  mdetunilem8  20647  ordtrest2lem  21229  ptpjpre1  21596  fbfinnfr  21866  filufint  21945  ptcmplem2  22078  cphsqrtcl3  23207  ovoliun  23493  voliunlem3  23540  volsup  23544  cxpsqrt  24669  amgm  24937  wilthlem2  25015  sqff1o  25128  chtublem  25156  bposlem1  25229  bposlem3  25231  ostth  25548  clwwisshclwwslemlem  27157  atdmd  29587  atmd2  29589  mdsymlem4  29595  ordtrest2NEWlem  30298  eulerpartlemb  30760  dfon2lem9  32022  nosupbnd1lem1  32181  nn0prpwlem  32644  ltflcei  33728  poimirlem30  33770  lplnexllnN  35371  2llnjaN  35373  paddasslem14  35640  cdleme32le  36255  dgrsub2  38225  iccelpart  41897  lighneallem3  42052  lighneal  42056
  Copyright terms: Public domain W3C validator