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 180
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  181  pm2.61d2  182  pm5.21ndd  381  bija  382  pm2.61dan  809  ecase3d  1026  pm2.61dne  3100  ordunidif  6232  dff3  6858  tfindsg  7564  findsg  7598  brtpos  7890  omwordi  8186  omass  8195  nnmwordi  8250  pssnn  8724  frfi  8751  ixpiunwdom  9043  cantnfp1lem3  9131  infxpenlem  9427  infxp  9625  ackbij1lem16  9645  axpowndlem3  10009  pwfseqlem4a  10071  gchina  10109  prlem936  10457  supsrlem  10521  flflp1  13165  hashunx  13735  swrdccat3blem  14089  repswswrd  14134  sumss  15069  fsumss  15070  prodss  15289  fprodss  15290  ruclem2  15573  prmind2  16017  rpexp  16052  fermltl  16109  prmreclem5  16244  ramcl  16353  wunress  16552  divsfval  16808  efgsfo  18794  lt6abl  18944  gsumval3  18956  mdetunilem8  21156  ordtrest2lem  21739  ptpjpre1  22107  fbfinnfr  22377  filufint  22456  ptcmplem2  22589  cphsqrtcl3  23718  ovoliun  24033  voliunlem3  24080  volsup  24084  cxpsqrt  25213  amgm  25495  wilthlem2  25573  sqff1o  25686  chtublem  25714  bposlem1  25787  bposlem3  25789  ostth  26142  clwwisshclwwslemlem  27718  atdmd  30102  atmd2  30104  mdsymlem4  30110  ordtrest2NEWlem  31064  eulerpartlemb  31525  dfon2lem9  32933  nosupbnd1lem1  33105  nn0prpwlem  33567  bj-ismooredr2  34296  ltflcei  34761  poimirlem30  34803  lplnexllnN  36580  2llnjaN  36582  paddasslem14  36849  cdleme32le  37463  dgrsub2  39613  iccelpart  43470  lighneallem3  43649  lighneal  43653
  Copyright terms: Public domain W3C validator