MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65i Structured version   Visualization version   GIF version

Theorem pm2.65i 185
Description: Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
pm2.65i.1 (𝜑𝜓)
pm2.65i.2 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.65i ¬ 𝜑

Proof of Theorem pm2.65i
StepHypRef Expression
1 pm2.65i.2 . . 3 (𝜑 → ¬ 𝜓)
21con2i 134 . 2 (𝜓 → ¬ 𝜑)
3 pm2.65i.1 . . 3 (𝜑𝜓)
43con3i 150 . 2 𝜓 → ¬ 𝜑)
52, 4pm2.61i 176 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.21dd  186  mto  188  mt2  191  noel  3901  0nelop  4930  canth  6573  sdom0  8052  canthwdom  8444  cardprclem  8765  ominf4  9094  canthp1lem2  9435  pwfseqlem4  9444  pwxpndom2  9447  lbioo  12164  ubioo  12165  fzp1disj  12357  fzonel  12440  fzouzdisj  12461  hashbclem  13190  harmonic  14535  eirrlem  14876  ruclem13  14915  prmreclem6  15568  4sqlem17  15608  vdwlem12  15639  vdwnnlem3  15644  mreexmrid  16243  psgnunilem3  17856  efgredlemb  18099  efgredlem  18100  00lss  18882  alexsublem  21788  ptcmplem4  21799  nmoleub2lem3  22855  dvferm1lem  23685  dvferm2lem  23687  plyeq0lem  23904  logno1  24316  lgsval2lem  24966  pntpbnd2  25210  ubico  29422  bnj1523  30900  pm2.65ni  38732  lbioc  39185  salgencntex  39898
  Copyright terms: Public domain W3C validator