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  2050  modal-b  2323  euae  2663  sbcbr123  5220  brabv  5588  elimasni  6121  ndmfvrcl  6956  oprssdm  7631  ndmovrcl  7636  omelon2  7916  omopthi  8717  fsetexb  8922  fsuppres  9462  sdomsdomcardi  10040  alephgeom  10151  rankcf  10846  adderpq  11025  mulerpq  11026  ssnn0fi  14036  sadcp1  16501  setcepi  18155  oduclatb  18577  cntzrcl  19367  pmtrfrn  19500  dprddomcld  20045  dprdsubg  20068  dsmmfi  21781  psrbagsn  22110  istps  22961  isusp  24291  dscmet  24606  dscopn  24607  i1f1lem  25743  sqff1o  27243  sltintdifex  27724  nolesgn2ores  27735  nogesgn1ores  27737  nosepdmlem  27746  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  upgrfi  29126  wwlksnndef  29938  dmadjrnb  31938  axpowprim  35666  opelco3  35738  bj-modal4e  36681  bj-snmooreb  37080  topdifinffinlem  37313  finxp1o  37358  ax6fromc10  38852  axc711to11  38873  axc5c711to11  38877  dffltz  42589  pw2f1ocnv  42994  kelac1  43020  relintabex  43543  axc5c4c711toc5  44371  axc5c4c711to11  44374  disjrnmpt2  45095  eubrv  46950  afvvdm  47056  afvvfunressn  47058  afvvv  47060  afvfv0bi  47067  dfatafv2rnb  47142  afv20defat  47147  fafv2elrnb  47150  afv2fv0  47180