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

Step	Hyp	Ref	Expression
1		con4i.1	. 2 ⊢ (¬ 𝜑 → ¬ 𝜓)
2		con4 113	. 2 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 → 𝜑)

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  2050  modal-b  2319  euae  2660  sbcbr123  5197  brabv  5573  elimasni  6109  ndmfvrcl  6942  oprssdm  7614  ndmovrcl  7619  omelon2  7900  omopthi  8699  fsetexb  8904  fsuppres  9433  sdomsdomcardi  10011  alephgeom  10122  rankcf  10817  adderpq  10996  mulerpq  10997  ssnn0fi  14026  sadcp1  16492  setcepi  18133  oduclatb  18552  cntzrcl  19345  pmtrfrn  19476  dprddomcld  20021  dprdsubg  20044  dsmmfi  21758  psrbagsn  22087  istps  22940  isusp  24270  dscmet  24585  dscopn  24586  i1f1lem  25724  sqff1o  27225  sltintdifex  27706  nolesgn2ores  27717  nogesgn1ores  27719  nosepdmlem  27728  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  upgrfi  29108  wwlksnndef  29925  dmadjrnb  31925  axpowprim  35704  opelco3  35775  bj-modal4e  36716  bj-snmooreb  37115  topdifinffinlem  37348  finxp1o  37393  ax6fromc10  38897  axc711to11  38918  axc5c711to11  38922  dffltz  42644  pw2f1ocnv  43049  kelac1  43075  relintabex  43594  axc5c4c711toc5  44421  axc5c4c711to11  44424  dfbi1ALTa  44960  simprimi  44961  disjrnmpt2  45193  eubrv  47047  afvvdm  47153  afvvfunressn  47155  afvvv  47157  afvfv0bi  47164  dfatafv2rnb  47239  afv20defat  47244  fafv2elrnb  47247  afv2fv0  47277