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 144 followed by nsyl2 143, 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  119  nsyl2  143  modal-b  2330  euae  2725  sbcbr123  5087  brabv  5421  elimasni  5927  ndmfvrcl  6680  oprssdm  7313  ndmovrcl  7318  omelon2  7576  omopthi  8271  fsuppres  8846  sdomsdomcardi  9388  alephgeom  9497  rankcf  10192  adderpq  10371  mulerpq  10372  ssnn0fi  13352  sadcp1  15797  setcepi  17343  oduclatb  17749  cntzrcl  18452  pmtrfrn  18581  dprddomcld  19119  dprdsubg  19142  dsmmfi  20430  psrbagsn  20737  istps  21542  isusp  22870  dscmet  23182  dscopn  23183  i1f1lem  24296  sqff1o  25770  upgrfi  26887  wwlksnndef  27694  dmadjrnb  29692  axpowprim  33038  opelco3  33126  sltintdifex  33276  nolesgn2ores  33287  nosepdmlem  33295  nosupbnd1lem3  33318  nosupbnd1lem5  33320  nosupbnd2lem1  33323  bj-modal4e  34157  bj-snmooreb  34524  topdifinffinlem  34759  finxp1o  34804  ax6fromc10  36185  axc711to11  36206  axc5c711to11  36210  dffltz  39602  pw2f1ocnv  39965  kelac1  39994  relintabex  40268  axc5c4c711toc5  41093  axc5c4c711to11  41096  disjrnmpt2  41802  eubrv  43614  afvvdm  43684  afvvfunressn  43686  afvvv  43688  afvfv0bi  43695  dfatafv2rnb  43770  afv20defat  43775  fafv2elrnb  43778  afv2fv0  43808
 Copyright terms: Public domain W3C validator