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  812  ecase3d  1030  pm2.61dne  3097  ordunidif  6217  dff3  6848  tfindsg  7560  findsg  7595  brtpos  7888  omwordi  8184  omass  8193  nnmwordi  8248  pssnn  8724  frfi  8751  ixpiunwdom  9042  cantnfp1lem3  9131  infxpenlem  9428  infxp  9626  ackbij1lem16  9646  axpowndlem3  10010  pwfseqlem4a  10072  gchina  10110  prlem936  10458  supsrlem  10522  flflp1  13172  hashunx  13743  swrdccat3blem  14092  repswswrd  14137  sumss  15072  fsumss  15073  prodss  15292  fprodss  15293  ruclem2  15576  prmind2  16018  rpexp  16053  fermltl  16110  prmreclem5  16245  ramcl  16354  wunress  16555  divsfval  16811  efgsfo  18856  lt6abl  19006  gsumval3  19018  mdetunilem8  21222  ordtrest2lem  21806  ptpjpre1  22174  fbfinnfr  22444  filufint  22523  ptcmplem2  22656  cphsqrtcl3  23790  ovoliun  24107  voliunlem3  24154  volsup  24158  cxpsqrt  25292  amgm  25574  wilthlem2  25652  sqff1o  25765  chtublem  25793  bposlem1  25866  bposlem3  25868  ostth  26221  clwwisshclwwslemlem  27796  atdmd  30179  atmd2  30181  mdsymlem4  30187  ordtrest2NEWlem  31239  eulerpartlemb  31700  dfon2lem9  33110  nosupbnd1lem1  33282  nn0prpwlem  33744  bj-ismooredr2  34486  ltflcei  35003  poimirlem30  35045  lplnexllnN  36818  2llnjaN  36820  paddasslem14  37087  cdleme32le  37701  dgrsub2  40009  iccelpart  43889  lighneallem3  44064  lighneal  44068
  Copyright terms: Public domain W3C validator