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 ⊢ (𝜓 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-3 8

This theorem is referenced by:  mt4  117  pm2.21i  120  nsyl2  142  19.8aw  2075  modal-b  2354  euae  2689  sbcbr123  5158  brabv  5541  elimasni  6083  ndmfvrcl  6904  oprssdm  7581  ndmovrcl  7586  omelon2  7863  omopthi  8635  fsetexb  8849  fsuppres  9341  sdomsdomcardi  9945  alephgeom  10054  rankcf  10750  adderpq  10929  mulerpq  10930  ssnn0fi  14009  sadcp1  16501  setcepi  18133  oduclatb  18551  chnfibg  18680  cntzrcl  19385  pmtrfrn  19516  dprddomcld  20061  dprdsubg  20084  dsmmfi  21845  psrbagsn  22171  istps  23048  isusp  24375  dscmet  24686  dscopn  24687  i1f1lem  25805  sqff1o  27300  ltsintdifex  27779  nolesgn2ores  27790  nogesgn1ores  27792  nosepdmlem  27801  nosupbnd1lem3  27828  nosupbnd1lem5  27830  nosupbnd2lem1  27833  noinfbnd1lem3  27843  noinfbnd1lem5  27845  noinfbnd2lem1  27848  upgrfi  29346  wwlksnndef  30159  dmadjrnb  32163  antnestlaw1  36049  antnestlaw2  36050  antnestlaw3  36051  axpowprim  36062  opelco3  36133  bj-modal4e  37199  bj-snmooreb  37611  topdifinffinlem  37848  finxp1o  37893  ax6fromc10  39527  axc711to11  39548  axc5c711to11  39552  dffltz  43223  pw2f1ocnv  43621  kelac1  43647  relintabex  44164  axc5c4c711toc5  44971  axc5c4c711to11  44974  dfbi1ALTa  45507  simprimi  45508  disjrnmpt2  45765  eubrv  47628  afvvdm  47734  afvvfunressn  47736  afvvv  47738  afvfv0bi  47745  dfatafv2rnb  47820  afv20defat  47825  fafv2elrnb  47828  afv2fv0  47858