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  2051  modal-b  2318  euae  2654  sbcbr123  5164  brabv  5531  elimasni  6065  ndmfvrcl  6897  oprssdm  7573  ndmovrcl  7578  omelon2  7858  omopthi  8628  fsetexb  8840  fsuppres  9351  sdomsdomcardi  9931  alephgeom  10042  rankcf  10737  adderpq  10916  mulerpq  10917  ssnn0fi  13957  sadcp1  16432  setcepi  18057  oduclatb  18473  cntzrcl  19266  pmtrfrn  19395  dprddomcld  19940  dprdsubg  19963  dsmmfi  21654  psrbagsn  21977  istps  22828  isusp  24156  dscmet  24467  dscopn  24468  i1f1lem  25597  sqff1o  27099  sltintdifex  27580  nolesgn2ores  27591  nogesgn1ores  27593  nosepdmlem  27602  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  upgrfi  29025  wwlksnndef  29842  dmadjrnb  31842  antnestlaw1  35685  antnestlaw2  35686  antnestlaw3  35687  axpowprim  35698  opelco3  35769  bj-modal4e  36710  bj-snmooreb  37109  topdifinffinlem  37342  finxp1o  37387  ax6fromc10  38896  axc711to11  38917  axc5c711to11  38921  dffltz  42629  pw2f1ocnv  43033  kelac1  43059  relintabex  43577  axc5c4c711toc5  44398  axc5c4c711to11  44401  dfbi1ALTa  44936  simprimi  44937  disjrnmpt2  45189  eubrv  47040  afvvdm  47146  afvvfunressn  47148  afvvv  47150  afvfv0bi  47157  dfatafv2rnb  47232  afv20defat  47237  fafv2elrnb  47240  afv2fv0  47270