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  2354  euae  2689  sbcbr123  5167  brabv  5553  elimasni  6095  ndmfvrcl  6918  oprssdm  7597  ndmovrcl  7602  omelon2  7877  omopthi  8649  fsetexb  8863  fsuppres  9356  sdomsdomcardi  9969  alephgeom  10078  rankcf  10773  adderpq  10952  mulerpq  10953  ssnn0fi  14034  sadcp1  16530  setcepi  18162  oduclatb  18580  chnfibg  18709  cntzrcl  19420  pmtrfrn  19551  dprddomcld  20096  dprdsubg  20119  dsmmfi  21917  psrbagsn  22243  istps  23120  isusp  24447  dscmet  24758  dscopn  24759  i1f1lem  25877  sqff1o  27375  ltsintdifex  27854  nolesgn2ores  27865  nogesgn1ores  27867  nosepdmlem  27876  nosupbnd1lem3  27903  nosupbnd1lem5  27905  nosupbnd2lem1  27908  noinfbnd1lem3  27918  noinfbnd1lem5  27920  noinfbnd2lem1  27923  upgrfi  29470  wwlksnndef  30283  dmadjrnb  32287  antnestlaw1  36196  antnestlaw2  36197  antnestlaw3  36198  axpowprim  36209  opelco3  36280  bj-modal4e  37375  bj-snmooreb  37789  topdifinffinlem  38026  finxp1o  38071  ax6fromc10  39703  axc711to11  39724  axc5c711to11  39728  dffltz  43399  pw2f1ocnv  43797  kelac1  43823  relintabex  44340  axc5c4c711toc5  45145  axc5c4c711to11  45148  dfbi1ALTa  45681  simprimi  45682  disjrnmpt2  45939  eubrv  47805  afvvdm  47911  afvvfunressn  47913  afvvv  47915  afvfv0bi  47922  dfatafv2rnb  47997  afv20defat  48002  fafv2elrnb  48005  afv2fv0  48035