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  37319  topdifinffinlem  37552  finxp1o  37597  ax6fromc10  39156  axc711to11  39177  axc5c711to11  39181  dffltz  42877  pw2f1ocnv  43279  kelac1  43305  relintabex  43822  axc5c4c711toc5  44643  axc5c4c711to11  44646  dfbi1ALTa  45180  simprimi  45181  disjrnmpt2  45432  eubrv  47281  afvvdm  47387  afvvfunressn  47389  afvvv  47391  afvfv0bi  47398  dfatafv2rnb  47473  afv20defat  47478  fafv2elrnb  47481  afv2fv0  47511