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  2053  modal-b  2324  euae  2660  sbcbr123  5152  brabv  5514  elimasni  6050  ndmfvrcl  6867  oprssdm  7539  ndmovrcl  7544  omelon2  7821  omopthi  8589  fsetexb  8801  fsuppres  9296  sdomsdomcardi  9883  alephgeom  9992  rankcf  10688  adderpq  10867  mulerpq  10868  ssnn0fi  13908  sadcp1  16382  setcepi  18012  oduclatb  18430  chnfibg  18559  cntzrcl  19256  pmtrfrn  19387  dprddomcld  19932  dprdsubg  19955  dsmmfi  21693  psrbagsn  22018  istps  22878  isusp  24205  dscmet  24516  dscopn  24517  i1f1lem  25646  sqff1o  27148  ltsintdifex  27629  nolesgn2ores  27640  nogesgn1ores  27642  nosepdmlem  27651  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  upgrfi  29164  wwlksnndef  29978  dmadjrnb  31981  antnestlaw1  35885  antnestlaw2  35886  antnestlaw3  35887  axpowprim  35898  opelco3  35969  bj-modal4e  36916  bj-snmooreb  37315  topdifinffinlem  37548  finxp1o  37593  ax6fromc10  39152  axc711to11  39173  axc5c711to11  39177  dffltz  42873  pw2f1ocnv  43275  kelac1  43301  relintabex  43818  axc5c4c711toc5  44639  axc5c4c711to11  44642  dfbi1ALTa  45176  simprimi  45177  disjrnmpt2  45428  eubrv  47277  afvvdm  47383  afvvfunressn  47385  afvvv  47387  afvfv0bi  47394  dfatafv2rnb  47469  afv20defat  47474  fafv2elrnb  47477  afv2fv0  47507