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  2322  euae  2657  sbcbr123  5149  brabv  5511  elimasni  6046  ndmfvrcl  6863  oprssdm  7535  ndmovrcl  7540  omelon2  7817  omopthi  8584  fsetexb  8796  fsuppres  9286  sdomsdomcardi  9873  alephgeom  9982  rankcf  10677  adderpq  10856  mulerpq  10857  ssnn0fi  13896  sadcp1  16370  setcepi  17999  oduclatb  18417  chnfibg  18546  cntzrcl  19243  pmtrfrn  19374  dprddomcld  19919  dprdsubg  19942  dsmmfi  21679  psrbagsn  22001  istps  22852  isusp  24179  dscmet  24490  dscopn  24491  i1f1lem  25620  sqff1o  27122  sltintdifex  27603  nolesgn2ores  27614  nogesgn1ores  27616  nosepdmlem  27625  nosupbnd1lem3  27652  nosupbnd1lem5  27654  nosupbnd2lem1  27657  noinfbnd1lem3  27667  noinfbnd1lem5  27669  noinfbnd2lem1  27672  upgrfi  29073  wwlksnndef  29887  dmadjrnb  31890  antnestlaw1  35758  antnestlaw2  35759  antnestlaw3  35760  axpowprim  35771  opelco3  35842  bj-modal4e  36782  bj-snmooreb  37181  topdifinffinlem  37414  finxp1o  37459  ax6fromc10  39018  axc711to11  39039  axc5c711to11  39043  dffltz  42755  pw2f1ocnv  43157  kelac1  43183  relintabex  43701  axc5c4c711toc5  44522  axc5c4c711to11  44525  dfbi1ALTa  45059  simprimi  45060  disjrnmpt2  45312  eubrv  47162  afvvdm  47268  afvvfunressn  47270  afvvv  47272  afvfv0bi  47279  dfatafv2rnb  47354  afv20defat  47359  fafv2elrnb  47362  afv2fv0  47392