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 182
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 147 . . 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  183  pm2.61d2  184  pm5.21ndd  384  bija  385  pm2.61dan  813  ecase3d  1034  ordunidif  6270  dff3  6928  tfindsg  7648  findsg  7686  brtpos  7986  omwordi  8308  omass  8317  nnmwordi  8372  pssnn  8857  pssnnOLD  8908  frfi  8929  ixpiunwdom  9219  cantnfp1lem3  9308  infxpenlem  9640  infxp  9842  ackbij1lem16  9862  axpowndlem3  10226  pwfseqlem4a  10288  gchina  10326  prlem936  10674  supsrlem  10738  flflp1  13395  hashunx  13966  swrdccat3blem  14317  repswswrd  14362  sumss  15301  fsumss  15302  prodss  15522  fprodss  15523  ruclem2  15806  prmind2  16255  rpexp  16292  fermltl  16350  prmreclem5  16486  ramcl  16595  wunress  16814  divsfval  17065  efgsfo  19142  lt6abl  19293  gsumval3  19305  mdetunilem8  21529  ordtrest2lem  22113  ptpjpre1  22481  fbfinnfr  22751  filufint  22830  ptcmplem2  22963  cphsqrtcl3  24097  ovoliun  24415  voliunlem3  24462  volsup  24466  cxpsqrt  25604  amgm  25886  wilthlem2  25964  sqff1o  26077  chtublem  26105  bposlem1  26178  bposlem3  26180  ostth  26533  clwwisshclwwslemlem  28109  atdmd  30492  atmd2  30494  mdsymlem4  30500  ordtrest2NEWlem  31599  eulerpartlemb  32060  fineqvac  32792  dfon2lem9  33499  nosupbnd1lem1  33661  noinfbnd1lem1  33676  nn0prpwlem  34261  bj-ismooredr2  35029  ltflcei  35515  poimirlem30  35557  lplnexllnN  37328  2llnjaN  37330  paddasslem14  37597  cdleme32le  38211  dgrsub2  40678  iccelpart  44573  lighneallem3  44747  lighneal  44751
  Copyright terms: Public domain W3C validator