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  831  ecase3d  983  axc11nlemOLD2  1985  axc11nlemOLD  2157  axc11nlemALT  2305  pm2.61dne  2876  ordunidif  5732  dff3  6328  tfindsg  7007  findsg  7040  brtpos  7306  omwordi  7596  omass  7605  nnmwordi  7660  pssnn  8122  frfi  8149  ixpiunwdom  8440  cantnfp1lem3  8521  infxpenlem  8780  infxp  8981  ackbij1lem16  9001  axpowndlem3  9365  pwfseqlem4a  9427  gchina  9465  prlem936  9813  supsrlem  9876  flflp1  12548  hashunx  13115  swrdccat3blem  13432  repswswrd  13468  sumss  14388  fsumss  14389  prodss  14602  fprodss  14603  ruclem2  14886  prmind2  15322  rpexp  15356  fermltl  15413  prmreclem5  15548  ramcl  15657  wunress  15861  divsfval  16128  efgsfo  18073  lt6abl  18217  gsumval3  18229  mdetunilem8  20344  ordtrest2lem  20917  ptpjpre1  21284  fbfinnfr  21555  filufint  21634  ptcmplem2  21767  cphsqrtcl3  22895  ovoliun  23180  voliunlem3  23227  volsup  23231  cxpsqrt  24349  amgm  24617  wilthlem2  24695  sqff1o  24808  chtublem  24836  bposlem1  24909  bposlem3  24911  ostth  25228  clwwisshclwwslemlem  26792  atdmd  29106  atmd2  29108  mdsymlem4  29114  ordtrest2NEWlem  29750  eulerpartlemb  30211  dfon2lem9  31397  nn0prpwlem  31959  ltflcei  33029  poimirlem30  33071  lplnexllnN  34330  2llnjaN  34332  paddasslem14  34599  cdleme32le  35215  dgrsub2  37186  iccelpart  40667  lighneallem3  40823  lighneal  40827
  Copyright terms: Public domain W3C validator