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  369  bija  370  pm2.61dan  832  ecase3d  984  axc11nlemOLD2  1987  axc11nlemOLD  2159  axc11nlemALT  2305  pm2.61dne  2879  ordunidif  5771  dff3  6370  tfindsg  7057  findsg  7090  brtpos  7358  omwordi  7648  omass  7657  nnmwordi  7712  pssnn  8175  frfi  8202  ixpiunwdom  8493  cantnfp1lem3  8574  infxpenlem  8833  infxp  9034  ackbij1lem16  9054  axpowndlem3  9418  pwfseqlem4a  9480  gchina  9518  prlem936  9866  supsrlem  9929  flflp1  12603  hashunx  13170  swrdccat3blem  13489  repswswrd  13525  sumss  14449  fsumss  14450  prodss  14671  fprodss  14672  ruclem2  14955  prmind2  15392  rpexp  15426  fermltl  15483  prmreclem5  15618  ramcl  15727  wunress  15934  divsfval  16201  efgsfo  18146  lt6abl  18290  gsumval3  18302  mdetunilem8  20419  ordtrest2lem  21001  ptpjpre1  21368  fbfinnfr  21639  filufint  21718  ptcmplem2  21851  cphsqrtcl3  22981  ovoliun  23267  voliunlem3  23314  volsup  23318  cxpsqrt  24443  amgm  24711  wilthlem2  24789  sqff1o  24902  chtublem  24930  bposlem1  25003  bposlem3  25005  ostth  25322  clwwisshclwwslemlem  26919  atdmd  29241  atmd2  29243  mdsymlem4  29249  ordtrest2NEWlem  29953  eulerpartlemb  30415  dfon2lem9  31680  nosupbnd1lem1  31838  nn0prpwlem  32301  ltflcei  33377  poimirlem30  33419  lplnexllnN  34676  2llnjaN  34678  paddasslem14  34945  cdleme32le  35561  dgrsub2  37531  iccelpart  41139  lighneallem3  41295  lighneal  41299
  Copyright terms: Public domain W3C validator