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  2056  modal-b  2316  euae  2662  sbcbr123  5132  brabv  5481  elimasni  5996  ndmfvrcl  6799  oprssdm  7444  ndmovrcl  7449  omelon2  7713  omopthi  8465  fsetexb  8626  fsuppres  9114  sdomsdomcardi  9713  alephgeom  9822  rankcf  10517  adderpq  10696  mulerpq  10697  ssnn0fi  13686  sadcp1  16143  setcepi  17784  oduclatb  18206  cntzrcl  18914  pmtrfrn  19047  dprddomcld  19585  dprdsubg  19608  dsmmfi  20926  psrbagsn  21252  istps  22064  isusp  23394  dscmet  23709  dscopn  23710  i1f1lem  24834  sqff1o  26312  upgrfi  27442  wwlksnndef  28249  dmadjrnb  30247  axpowprim  33624  opelco3  33728  sltintdifex  33843  nolesgn2ores  33854  nogesgn1ores  33856  nosepdmlem  33865  nosupbnd1lem3  33892  nosupbnd1lem5  33894  nosupbnd2lem1  33897  noinfbnd1lem3  33907  noinfbnd1lem5  33909  noinfbnd2lem1  33912  bj-modal4e  34876  bj-snmooreb  35264  topdifinffinlem  35497  finxp1o  35542  ax6fromc10  36889  axc711to11  36910  axc5c711to11  36914  dffltz  40451  pw2f1ocnv  40839  kelac1  40868  relintabex  41142  axc5c4c711toc5  41973  axc5c4c711to11  41976  disjrnmpt2  42679  eubrv  44480  afvvdm  44584  afvvfunressn  44586  afvvv  44588  afvfv0bi  44595  dfatafv2rnb  44670  afv20defat  44675  fafv2elrnb  44678  afv2fv0  44708