Theorem con4i 114

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

Remark: this can also be proved using notnot 144 followed by nsyl2 143, 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  143  modal-b  2320  euae  2660  sbcbr123  5093  brabv  5433  elimasni  5941  ndmfvrcl  6726  oprssdm  7367  ndmovrcl  7372  omelon2  7635  omopthi  8364  fsetexb  8523  fsuppres  8988  sdomsdomcardi  9552  alephgeom  9661  rankcf  10356  adderpq  10535  mulerpq  10536  ssnn0fi  13523  sadcp1  15977  setcepi  17548  oduclatb  17967  cntzrcl  18675  pmtrfrn  18804  dprddomcld  19342  dprdsubg  19365  dsmmfi  20654  psrbagsn  20975  istps  21785  isusp  23113  dscmet  23424  dscopn  23425  i1f1lem  24540  sqff1o  26018  upgrfi  27136  wwlksnndef  27943  dmadjrnb  29941  axpowprim  33312  opelco3  33419  sltintdifex  33550  nolesgn2ores  33561  nogesgn1ores  33563  nosepdmlem  33572  nosupbnd1lem3  33599  nosupbnd1lem5  33601  nosupbnd2lem1  33604  noinfbnd1lem3  33614  noinfbnd1lem5  33616  noinfbnd2lem1  33619  bj-modal4e  34583  bj-snmooreb  34969  topdifinffinlem  35204  finxp1o  35249  ax6fromc10  36596  axc711to11  36617  axc5c711to11  36621  19.8aw  39841  dffltz  40115  pw2f1ocnv  40503  kelac1  40532  relintabex  40806  axc5c4c711toc5  41634  axc5c4c711to11  41637  disjrnmpt2  42340  eubrv  44144  afvvdm  44248  afvvfunressn  44250  afvvv  44252  afvfv0bi  44259  dfatafv2rnb  44334  afv20defat  44339  fafv2elrnb  44342  afv2fv0  44372