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 142 followed by nsyl2 141, 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  141  19.8aw  2053  modal-b  2312  euae  2659  sbcbr123  5159  brabv  5526  elimasni  6043  ndmfvrcl  6878  oprssdm  7534  ndmovrcl  7539  omelon2  7814  omopthi  8606  fsetexb  8801  fsuppres  9329  sdomsdomcardi  9906  alephgeom  10017  rankcf  10712  adderpq  10891  mulerpq  10892  ssnn0fi  13889  sadcp1  16334  setcepi  17973  oduclatb  18395  cntzrcl  19105  pmtrfrn  19238  dprddomcld  19778  dprdsubg  19801  dsmmfi  21142  psrbagsn  21469  istps  22281  isusp  23611  dscmet  23926  dscopn  23927  i1f1lem  25051  sqff1o  26529  sltintdifex  27007  nolesgn2ores  27018  nogesgn1ores  27020  nosepdmlem  27029  nosupbnd1lem3  27056  nosupbnd1lem5  27058  nosupbnd2lem1  27061  noinfbnd1lem3  27071  noinfbnd1lem5  27073  noinfbnd2lem1  27076  upgrfi  27989  wwlksnndef  28797  dmadjrnb  30795  axpowprim  34215  opelco3  34289  bj-modal4e  35170  bj-snmooreb  35575  topdifinffinlem  35808  finxp1o  35853  ax6fromc10  37348  axc711to11  37369  axc5c711to11  37373  dffltz  40949  pw2f1ocnv  41338  kelac1  41367  relintabex  41834  axc5c4c711toc5  42663  axc5c4c711to11  42666  disjrnmpt2  43382  eubrv  45240  afvvdm  45344  afvvfunressn  45346  afvvv  45348  afvfv0bi  45355  dfatafv2rnb  45430  afv20defat  45435  fafv2elrnb  45438  afv2fv0  45468
  Copyright terms: Public domain W3C validator