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  2142  sbcbr123  4706  elimasni  5492  ndmfvrcl  6219  brabv  6699  oprssdm  6815  ndmovrcl  6820  omelon2  7077  omopthi  7737  fsuppres  8300  sdomsdomcardi  8797  alephgeom  8905  pwcdadom  9038  rankcf  9599  adderpq  9778  mulerpq  9779  ssnn0fi  12784  sadcp1  15177  setcepi  16738  oduclatb  17144  cntzrcl  17760  pmtrfrn  17878  dprddomcld  18400  dprdsubg  18423  psrbagsn  19495  dsmmbas2  20081  dsmmfi  20082  istps  20738  isusp  22065  dscmet  22377  dscopn  22378  i1f1lem  23456  sqff1o  24908  upgrfi  25986  wwlksnndef  26800  clwwlksnndef  26890  dmadjrnb  28765  axpowprim  31581  opelco3  31678  sltintdifex  31814  nolesgn2ores  31825  nosepdmlem  31833  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  bj-modal5e  32636  bj-modal4e  32705  bj-snmoore  33068  topdifinffinlem  33195  finxp1o  33229  ax6fromc10  34181  axc711to11  34202  axc5c711to11  34206  pw2f1ocnv  37604  kelac1  37633  relintabex  37887  axc5c4c711toc5  38603  axc5c4c711to11  38606  disjrnmpt2  39375  afvvdm  41221  afvvfunressn  41223  afvvv  41225  afvfv0bi  41232