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  2315  sbcbr123  4862  elimasni  5673  ndmfvrcl  6405  brabv  6896  oprssdm  7012  ndmovrcl  7017  omelon2  7274  omopthi  7941  fsuppres  8506  sdomsdomcardi  9047  alephgeom  9155  pwcdadom  9290  rankcf  9851  adderpq  10030  mulerpq  10031  ssnn0fi  12991  sadcp1  15459  setcepi  17004  oduclatb  17411  cntzrcl  18024  pmtrfrn  18142  dprddomcld  18666  dprdsubg  18689  psrbagsn  19767  dsmmbas2  20356  dsmmfi  20357  istps  21017  isusp  22343  dscmet  22655  dscopn  22656  i1f1lem  23746  sqff1o  25198  upgrfi  26262  wwlksnndef  27104  dmadjrnb  29155  axpowprim  31958  opelco3  32052  sltintdifex  32189  nolesgn2ores  32200  nosepdmlem  32208  nosupbnd1lem3  32231  nosupbnd1lem5  32233  nosupbnd2lem1  32236  bj-modal4e  33071  bj-snmoore  33428  topdifinffinlem  33560  finxp1o  33594  ax6fromc10  34784  axc711to11  34805  axc5c711to11  34809  pw2f1ocnv  38213  kelac1  38242  relintabex  38494  axc5c4c711toc5  39208  axc5c4c711to11  39211  disjrnmpt2  39954  eubrv  41744  afvvdm  41821  afvvfunressn  41823  afvvv  41825  afvfv0bi  41832  dfatafv2rnb  41907  afv20defat  41912  fafv2elrnb  41915  afv2fv0  41945
  Copyright terms: Public domain W3C validator