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  2082  modal-b  2352  euae  2687  sbcbr123  5166  brabv  5553  elimasni  6095  ndmfvrcl  6916  oprssdm  7593  ndmovrcl  7598  omelon2  7876  omopthi  8648  fsetexb  8862  fsuppres  9354  sdomsdomcardi  9958  alephgeom  10067  rankcf  10763  adderpq  10942  mulerpq  10943  ssnn0fi  14023  sadcp1  16514  setcepi  18146  oduclatb  18564  chnfibg  18693  cntzrcl  19398  pmtrfrn  19529  dprddomcld  20074  dprdsubg  20097  dsmmfi  21869  psrbagsn  22195  istps  23072  isusp  24399  dscmet  24710  dscopn  24711  i1f1lem  25829  sqff1o  27327  ltsintdifex  27806  nolesgn2ores  27817  nogesgn1ores  27819  nosepdmlem  27828  nosupbnd1lem3  27855  nosupbnd1lem5  27857  nosupbnd2lem1  27860  noinfbnd1lem3  27870  noinfbnd1lem5  27872  noinfbnd2lem1  27875  upgrfi  29422  wwlksnndef  30235  dmadjrnb  32239  antnestlaw1  36164  antnestlaw2  36165  antnestlaw3  36166  axpowprim  36177  opelco3  36248  bj-modal4e  37323  bj-snmooreb  37737  topdifinffinlem  37974  finxp1o  38019  ax6fromc10  39651  axc711to11  39672  axc5c711to11  39676  dffltz  43349  pw2f1ocnv  43747  kelac1  43773  relintabex  44290  axc5c4c711toc5  45095  axc5c4c711to11  45098  dfbi1ALTa  45631  simprimi  45632  disjrnmpt2  45889  eubrv  47755  afvvdm  47861  afvvfunressn  47863  afvvv  47865  afvfv0bi  47872  dfatafv2rnb  47947  afv20defat  47952  fafv2elrnb  47955  afv2fv0  47985