Theorem con4i 115

Description: Inference associated with con4 114. Its associated inference is mt4 117.

Remark: this can also be proved using notnot 143 followed by nsyl2 142, 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 114	. 2 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-3 8

This theorem is used by:  mt4  117  pm2.21i  120  nsyl2  142  19.8aw  2085  modal-b  2350  euae  2685  sbcbr123  5159  brabv  5541  elimasni  6089  ndmfvrcl  6916  oprssdm  7600  ndmovrcl  7605  omelon2  7888  omopthi  8663  fsetexb  8879  fsuppres  9378  sdomsdomcardi  10045  alephgeom  10154  rankcf  10855  adderpq  11034  mulerpq  11035  ssnn0fi  14121  sadcp1  16618  setcepi  18256  oduclatb  18674  chnfibg  18803  cntzrcl  19534  pmtrfrn  19665  dprddomcld  20210  dprdsubg  20233  dsmmfi  22037  psrbagsn  22365  istps  23245  isusp  24573  dscmet  24884  dscopn  24885  i1f1lem  26003  sqff1o  27502  ltsintdifex  28011  nolesgn2ores  28022  nogesgn1ores  28024  nosepdmlem  28033  nosupbnd1lem3  28060  nosupbnd1lem5  28062  nosupbnd2lem1  28065  noinfbnd1lem3  28075  noinfbnd1lem5  28077  noinfbnd2lem1  28080  upgrfi  29662  wwlksnndef  30487  dmadjrnb  32501  antnestlaw1  36435  antnestlaw2  36436  antnestlaw3  36437  axpowprim  36448  opelco3  36519  bj-modal4e  37599  bj-snmooreb  38015  topdifinffinlem  38250  finxp1o  38295  ax6fromc10  39933  axc711to11  39954  axc5c711to11  39958  dffltz  43650  pw2f1ocnv  44023  kelac1  44049  relintabex  44566  axc5c4c711toc5  45371  axc5c4c711to11  45374  dfbi1ALTa  45907  simprimi  45908  disjrnmpt2  46172  eubrv  48074  afvvdm  48180  afvvfunressn  48182  afvvv  48184  afvfv0bi  48191  dfatafv2rnb  48266  afv20defat  48271  fafv2elrnb  48274  afv2fv0  48304