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  2047  modal-b  2317  euae  2657  sbcbr123  5201  brabv  5577  elimasni  6111  ndmfvrcl  6942  oprssdm  7613  ndmovrcl  7618  omelon2  7899  omopthi  8697  fsetexb  8902  fsuppres  9430  sdomsdomcardi  10008  alephgeom  10119  rankcf  10814  adderpq  10993  mulerpq  10994  ssnn0fi  14022  sadcp1  16488  setcepi  18141  oduclatb  18564  cntzrcl  19357  pmtrfrn  19490  dprddomcld  20035  dprdsubg  20058  dsmmfi  21775  psrbagsn  22104  istps  22955  isusp  24285  dscmet  24600  dscopn  24601  i1f1lem  25737  sqff1o  27239  sltintdifex  27720  nolesgn2ores  27731  nogesgn1ores  27733  nosepdmlem  27742  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  upgrfi  29122  wwlksnndef  29934  dmadjrnb  31934  axpowprim  35683  opelco3  35755  bj-modal4e  36697  bj-snmooreb  37096  topdifinffinlem  37329  finxp1o  37374  ax6fromc10  38877  axc711to11  38898  axc5c711to11  38902  dffltz  42620  pw2f1ocnv  43025  kelac1  43051  relintabex  43570  axc5c4c711toc5  44397  axc5c4c711to11  44400  disjrnmpt2  45130  eubrv  46984  afvvdm  47090  afvvfunressn  47092  afvvv  47094  afvfv0bi  47101  dfatafv2rnb  47176  afv20defat  47181  fafv2elrnb  47184  afv2fv0  47214