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  2054  modal-b  2313  euae  2656  sbcbr123  5203  brabv  5570  elimasni  6091  ndmfvrcl  6928  oprssdm  7588  ndmovrcl  7593  omelon2  7868  omopthi  8660  fsetexb  8858  fsuppres  9388  sdomsdomcardi  9966  alephgeom  10077  rankcf  10772  adderpq  10951  mulerpq  10952  ssnn0fi  13950  sadcp1  16396  setcepi  18038  oduclatb  18460  cntzrcl  19191  pmtrfrn  19326  dprddomcld  19871  dprdsubg  19894  dsmmfi  21293  psrbagsn  21624  istps  22436  isusp  23766  dscmet  24081  dscopn  24082  i1f1lem  25206  sqff1o  26686  sltintdifex  27164  nolesgn2ores  27175  nogesgn1ores  27177  nosepdmlem  27186  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  upgrfi  28351  wwlksnndef  29159  dmadjrnb  31159  axpowprim  34673  opelco3  34746  bj-modal4e  35593  bj-snmooreb  35995  topdifinffinlem  36228  finxp1o  36273  ax6fromc10  37766  axc711to11  37787  axc5c711to11  37791  dffltz  41376  pw2f1ocnv  41776  kelac1  41805  relintabex  42332  axc5c4c711toc5  43161  axc5c4c711to11  43164  disjrnmpt2  43886  eubrv  45745  afvvdm  45849  afvvfunressn  45851  afvvv  45853  afvfv0bi  45860  dfatafv2rnb  45935  afv20defat  45940  fafv2elrnb  45943  afv2fv0  45973