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  2054  modal-b  2325  euae  2661  sbcbr123  5140  brabv  5514  elimasni  6050  ndmfvrcl  6867  oprssdm  7541  ndmovrcl  7546  omelon2  7823  omopthi  8590  fsetexb  8804  fsuppres  9299  sdomsdomcardi  9886  alephgeom  9995  rankcf  10691  adderpq  10870  mulerpq  10871  ssnn0fi  13938  sadcp1  16415  setcepi  18046  oduclatb  18464  chnfibg  18593  cntzrcl  19293  pmtrfrn  19424  dprddomcld  19969  dprdsubg  19992  dsmmfi  21728  psrbagsn  22051  istps  22909  isusp  24236  dscmet  24547  dscopn  24548  i1f1lem  25666  sqff1o  27159  ltsintdifex  27639  nolesgn2ores  27650  nogesgn1ores  27652  nosepdmlem  27661  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  upgrfi  29174  wwlksnndef  29988  dmadjrnb  31992  antnestlaw1  35889  antnestlaw2  35890  antnestlaw3  35891  axpowprim  35902  opelco3  35973  bj-modal4e  37030  bj-snmooreb  37442  topdifinffinlem  37677  finxp1o  37722  ax6fromc10  39356  axc711to11  39377  axc5c711to11  39381  dffltz  43081  pw2f1ocnv  43483  kelac1  43509  relintabex  44026  axc5c4c711toc5  44847  axc5c4c711to11  44850  dfbi1ALTa  45384  simprimi  45385  disjrnmpt2  45636  eubrv  47495  afvvdm  47601  afvvfunressn  47603  afvvv  47605  afvfv0bi  47612  dfatafv2rnb  47687  afv20defat  47692  fafv2elrnb  47695  afv2fv0  47725