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

Theorem con4i 114
Description: Inference associated with con4 113. Its associated inference is mt4 116.

Remark: this can also be proved using notnot 138 followed by nsyl2 144, giving a shorter proof but depending on more axioms (namely, ax-1 6 and ax-2 7). (Contributed by NM, 29-Dec-1992.)

Hypothesis
Ref Expression
con4i.1 𝜑 → ¬ 𝜓)
Assertion
Ref Expression
con4i (𝜓𝜑)

Proof of Theorem con4i
StepHypRef Expression
1 con4i.1 . 2 𝜑 → ¬ 𝜓)
2 con4 113 . 2 ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-3 8
This theorem is referenced by:  mt4  116  pm2.21i  117  modal-b  2310  sbcbr123  4851  elimasni  5643  ndmfvrcl  6377  brabv  6867  oprssdm  6983  ndmovrcl  6988  omelon2  7245  omopthi  7912  fsuppres  8477  sdomsdomcardi  9018  alephgeom  9126  pwcdadom  9261  rankcf  9822  adderpq  10001  mulerpq  10002  ssnn0fi  13014  sadcp1  15406  setcepi  16965  oduclatb  17372  cntzrcl  17987  pmtrfrn  18105  dprddomcld  18628  dprdsubg  18651  psrbagsn  19730  dsmmbas2  20318  dsmmfi  20319  istps  20979  isusp  22305  dscmet  22617  dscopn  22618  i1f1lem  23697  sqff1o  25150  upgrfi  26228  wwlksnndef  27070  dmadjrnb  29122  axpowprim  31936  opelco3  32031  sltintdifex  32168  nolesgn2ores  32179  nosepdmlem  32187  nosupbnd1lem3  32210  nosupbnd1lem5  32212  nosupbnd2lem1  32215  bj-modal4e  33058  bj-snmoore  33417  topdifinffinlem  33549  finxp1o  33583  ax6fromc10  34719  axc711to11  34740  axc5c711to11  34744  pw2f1ocnv  38145  kelac1  38174  relintabex  38427  axc5c4c711toc5  39142  axc5c4c711to11  39145  disjrnmpt2  39906  afvvdm  41766  afvvfunressn  41768  afvvv  41770  afvfv0bi  41777
  Copyright terms: Public domain W3C validator