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 127 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  370  bija  371  pm2.61dan  847  ecase3d  1057  pm2.61dne  3023  ordunidif  5956  dff3  6562  tfindsg  7258  findsg  7291  brtpos  7564  omwordi  7856  omass  7865  nnmwordi  7920  pssnn  8385  frfi  8412  ixpiunwdom  8703  cantnfp1lem3  8792  infxpenlem  9087  infxp  9290  ackbij1lem16  9310  axpowndlem3  9674  pwfseqlem4a  9736  gchina  9774  prlem936  10122  supsrlem  10185  flflp1  12816  hashunx  13377  swrdccat3blem  13749  repswswrd  13808  sumss  14740  fsumss  14741  prodss  14960  fprodss  14961  ruclem2  15243  prmind2  15678  rpexp  15711  fermltl  15768  prmreclem5  15903  ramcl  16012  wunress  16213  divsfval  16473  efgsfo  18417  lt6abl  18562  gsumval3  18574  mdetunilem8  20702  ordtrest2lem  21287  ptpjpre1  21654  fbfinnfr  21924  filufint  22003  ptcmplem2  22136  cphsqrtcl3  23265  ovoliun  23563  voliunlem3  23610  volsup  23614  cxpsqrt  24740  amgm  25008  wilthlem2  25086  sqff1o  25199  chtublem  25227  bposlem1  25300  bposlem3  25302  ostth  25619  clwwisshclwwslemlem  27249  atdmd  29713  atmd2  29715  mdsymlem4  29721  ordtrest2NEWlem  30415  eulerpartlemb  30877  dfon2lem9  32139  nosupbnd1lem1  32298  nn0prpwlem  32760  ltflcei  33821  poimirlem30  33863  lplnexllnN  35520  2llnjaN  35522  paddasslem14  35789  cdleme32le  36403  dgrsub2  38382  iccelpart  42103  lighneallem3  42200  lighneal  42204
  Copyright terms: Public domain W3C validator