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  2324  euae  2660  sbcbr123  5139  brabv  5521  elimasni  6056  ndmfvrcl  6873  oprssdm  7548  ndmovrcl  7553  omelon2  7830  omopthi  8597  fsetexb  8811  fsuppres  9306  sdomsdomcardi  9895  alephgeom  10004  rankcf  10700  adderpq  10879  mulerpq  10880  ssnn0fi  13947  sadcp1  16424  setcepi  18055  oduclatb  18473  chnfibg  18602  cntzrcl  19302  pmtrfrn  19433  dprddomcld  19978  dprdsubg  20001  dsmmfi  21718  psrbagsn  22041  istps  22899  isusp  24226  dscmet  24537  dscopn  24538  i1f1lem  25656  sqff1o  27145  ltsintdifex  27625  nolesgn2ores  27636  nogesgn1ores  27638  nosepdmlem  27647  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  upgrfi  29160  wwlksnndef  29973  dmadjrnb  31977  antnestlaw1  35873  antnestlaw2  35874  antnestlaw3  35875  axpowprim  35886  opelco3  35957  bj-modal4e  37014  bj-snmooreb  37426  topdifinffinlem  37663  finxp1o  37708  ax6fromc10  39342  axc711to11  39363  axc5c711to11  39367  dffltz  43067  pw2f1ocnv  43465  kelac1  43491  relintabex  44008  axc5c4c711toc5  44829  axc5c4c711to11  44832  dfbi1ALTa  45366  simprimi  45367  disjrnmpt2  45618  eubrv  47483  afvvdm  47589  afvvfunressn  47591  afvvv  47593  afvfv0bi  47600  dfatafv2rnb  47675  afv20defat  47680  fafv2elrnb  47683  afv2fv0  47713