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  2051  modal-b  2318  euae  2653  sbcbr123  5161  brabv  5528  elimasni  6062  ndmfvrcl  6894  oprssdm  7570  ndmovrcl  7575  omelon2  7855  omopthi  8625  fsetexb  8837  fsuppres  9344  sdomsdomcardi  9924  alephgeom  10035  rankcf  10730  adderpq  10909  mulerpq  10910  ssnn0fi  13950  sadcp1  16425  setcepi  18050  oduclatb  18466  cntzrcl  19259  pmtrfrn  19388  dprddomcld  19933  dprdsubg  19956  dsmmfi  21647  psrbagsn  21970  istps  22821  isusp  24149  dscmet  24460  dscopn  24461  i1f1lem  25590  sqff1o  27092  sltintdifex  27573  nolesgn2ores  27584  nogesgn1ores  27586  nosepdmlem  27595  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  upgrfi  29018  wwlksnndef  29835  dmadjrnb  31835  antnestlaw1  35678  antnestlaw2  35679  antnestlaw3  35680  axpowprim  35691  opelco3  35762  bj-modal4e  36703  bj-snmooreb  37102  topdifinffinlem  37335  finxp1o  37380  ax6fromc10  38889  axc711to11  38910  axc5c711to11  38914  dffltz  42622  pw2f1ocnv  43026  kelac1  43052  relintabex  43570  axc5c4c711toc5  44391  axc5c4c711to11  44394  dfbi1ALTa  44929  simprimi  44930  disjrnmpt2  45182  eubrv  47036  afvvdm  47142  afvvfunressn  47144  afvvv  47146  afvfv0bi  47153  dfatafv2rnb  47228  afv20defat  47233  fafv2elrnb  47236  afv2fv0  47266