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  2071  modal-b  2350  euae  2685  sbcbr123  5151  brabv  5533  elimasni  6075  ndmfvrcl  6894  oprssdm  7571  ndmovrcl  7576  omelon2  7853  omopthi  8624  fsetexb  8838  fsuppres  9332  sdomsdomcardi  9922  alephgeom  10031  rankcf  10728  adderpq  10907  mulerpq  10908  ssnn0fi  13991  sadcp1  16479  setcepi  18111  oduclatb  18529  chnfibg  18658  cntzrcl  19357  pmtrfrn  19488  dprddomcld  20033  dprdsubg  20056  dsmmfi  21777  psrbagsn  22103  istps  22981  isusp  24308  dscmet  24619  dscopn  24620  i1f1lem  25738  sqff1o  27233  ltsintdifex  27712  nolesgn2ores  27723  nogesgn1ores  27725  nosepdmlem  27734  nosupbnd1lem3  27761  nosupbnd1lem5  27763  nosupbnd2lem1  27766  noinfbnd1lem3  27776  noinfbnd1lem5  27778  noinfbnd2lem1  27781  upgrfi  29248  wwlksnndef  30061  dmadjrnb  32065  antnestlaw1  36001  antnestlaw2  36002  antnestlaw3  36003  axpowprim  36014  opelco3  36085  bj-modal4e  37152  bj-snmooreb  37564  topdifinffinlem  37801  finxp1o  37846  ax6fromc10  39480  axc711to11  39501  axc5c711to11  39505  dffltz  43176  pw2f1ocnv  43574  kelac1  43600  relintabex  44117  axc5c4c711toc5  44938  axc5c4c711to11  44941  dfbi1ALTa  45475  simprimi  45476  disjrnmpt2  45726  eubrv  47589  afvvdm  47695  afvvfunressn  47697  afvvv  47699  afvfv0bi  47706  dfatafv2rnb  47781  afv20defat  47786  fafv2elrnb  47789  afv2fv0  47819