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  2059  modal-b  2328  euae  2664  sbcbr123  5133  brabv  5515  elimasni  6050  ndmfvrcl  6867  oprssdm  7544  ndmovrcl  7549  omelon2  7826  omopthi  8594  fsetexb  8808  fsuppres  9303  sdomsdomcardi  9893  alephgeom  10002  rankcf  10698  adderpq  10877  mulerpq  10878  ssnn0fi  13945  sadcp1  16422  setcepi  18053  oduclatb  18471  chnfibg  18600  cntzrcl  19300  pmtrfrn  19431  dprddomcld  19976  dprdsubg  19999  dsmmfi  21720  psrbagsn  22046  istps  22924  isusp  24251  dscmet  24562  dscopn  24563  i1f1lem  25681  sqff1o  27170  ltsintdifex  27650  nolesgn2ores  27661  nogesgn1ores  27663  nosepdmlem  27672  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  upgrfi  29185  wwlksnndef  29998  dmadjrnb  32002  antnestlaw1  35926  antnestlaw2  35927  antnestlaw3  35928  axpowprim  35939  opelco3  36010  bj-modal4e  37067  bj-snmooreb  37479  topdifinffinlem  37716  finxp1o  37761  ax6fromc10  39395  axc711to11  39416  axc5c711to11  39420  dffltz  43091  pw2f1ocnv  43489  kelac1  43515  relintabex  44032  axc5c4c711toc5  44853  axc5c4c711to11  44856  dfbi1ALTa  45390  simprimi  45391  disjrnmpt2  45642  eubrv  47505  afvvdm  47611  afvvfunressn  47613  afvvv  47615  afvfv0bi  47622  dfatafv2rnb  47697  afv20defat  47702  fafv2elrnb  47705  afv2fv0  47735