Theorem con4i 114

Description: Inference associated with con4 113. Its associated inference is mt4 116.

Remark: this can also be proved using notnot 139 followed by nsyl2 145, 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  117  modal-b  2257  euae  2686  sbcbr123  4977  brabv  5298  elimasni  5790  ndmfvrcl  6524  oprssdm  7139  ndmovrcl  7144  omelon2  7402  omopthi  8076  fsuppres  8645  sdomsdomcardi  9186  alephgeom  9294  rankcf  9989  adderpq  10168  mulerpq  10169  ssnn0fi  13161  sadcp1  15654  setcepi  17196  oduclatb  17602  cntzrcl  18218  pmtrfrn  18337  dprddomcld  18863  dprdsubg  18886  psrbagsn  19978  dsmmbas2  20573  dsmmfi  20574  istps  21236  isusp  22563  dscmet  22875  dscopn  22876  i1f1lem  23983  sqff1o  25451  upgrfi  26569  wwlksnndef  27394  dmadjrnb  29454  axpowprim  32390  opelco3  32478  sltintdifex  32629  nolesgn2ores  32640  nosepdmlem  32648  nosupbnd1lem3  32671  nosupbnd1lem5  32673  nosupbnd2lem1  32676  bj-modal4e  33497  bj-snmoore  33851  topdifinffinlem  34005  finxp1o  34049  ax6fromc10  35425  axc711to11  35446  axc5c711to11  35450  dffltz  38623  pw2f1ocnv  38975  kelac1  39004  relintabex  39248  axc5c4c711toc5  40095  axc5c4c711to11  40098  disjrnmpt2  40819  eubrv  42621  afvvdm  42692  afvvfunressn  42694  afvvv  42696  afvfv0bi  42703  dfatafv2rnb  42778  afv20defat  42783  fafv2elrnb  42786  afv2fv0  42816