Theorem con4i 113

Description: Inference associated with con4 112. Its associated inference is mt4 115.

Remark: this can also be proved using notnot 136 followed by nsyl2 142, 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 112	. 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  115  pm2.21i  116  modal-b  2180  sbcbr123  4739  elimasni  5527  ndmfvrcl  6257  brabv  6741  oprssdm  6857  ndmovrcl  6862  omelon2  7119  omopthi  7782  fsuppres  8341  sdomsdomcardi  8835  alephgeom  8943  pwcdadom  9076  rankcf  9637  adderpq  9816  mulerpq  9817  ssnn0fi  12824  sadcp1  15224  setcepi  16785  oduclatb  17191  cntzrcl  17806  pmtrfrn  17924  dprddomcld  18446  dprdsubg  18469  psrbagsn  19543  dsmmbas2  20129  dsmmfi  20130  istps  20786  isusp  22112  dscmet  22424  dscopn  22425  i1f1lem  23501  sqff1o  24953  upgrfi  26031  wwlksnndef  26868  dmadjrnb  28893  axpowprim  31707  opelco3  31802  sltintdifex  31939  nolesgn2ores  31950  nosepdmlem  31958  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2lem1  31986  bj-modal5e  32761  bj-modal4e  32830  bj-snmoore  33193  topdifinffinlem  33325  finxp1o  33359  ax6fromc10  34500  axc711to11  34521  axc5c711to11  34525  pw2f1ocnv  37921  kelac1  37950  relintabex  38204  axc5c4c711toc5  38920  axc5c4c711to11  38923  disjrnmpt2  39689  afvvdm  41542  afvvfunressn  41544  afvvv  41546  afvfv0bi  41553