Theorem con4i 113

Description: Inference associated with con4 112. Its associated inference is mt4 115. (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 112	. 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  115  pm2.21i  116  modal-b  2143  sbcbr123  4671  elimasni  5455  ndmfvrcl  6177  brabv  6653  oprssdm  6769  ndmovrcl  6774  omelon2  7025  omopthi  7683  fsuppres  8245  sdomsdomcardi  8742  alephgeom  8850  pwcdadom  8983  rankcf  9544  adderpq  9723  mulerpq  9724  ssnn0fi  12721  sadcp1  15096  setcepi  16654  oduclatb  17060  cntzrcl  17676  pmtrfrn  17794  dprddomcld  18316  dprdsubg  18339  psrbagsn  19409  dsmmbas2  19995  dsmmfi  19996  istps  20646  isusp  21970  dscmet  22282  dscopn  22283  i1f1lem  23357  sqff1o  24803  upgrfi  25877  wwlksnndef  26663  clwwlksnndef  26751  dmadjrnb  28605  axpowprim  31281  opelco3  31372  sltintdifex  31509  nosepdmlem  31559  bj-modal5e  32270  bj-modal4e  32339  topdifinffinlem  32819  finxp1o  32853  ax6fromc10  33647  axc711to11  33668  axc5c711to11  33672  pw2f1ocnv  37070  kelac1  37099  relintabex  37354  axc5c4c711toc5  38071  axc5c4c711to11  38074  disjrnmpt2  38835  afvvdm  40512  afvvfunressn  40514  afvvv  40516  afvfv0bi  40523