Theorem con4i 112

Description: Inference associated with con4 111. Its associated inference is mt4 114. (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 111	. 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  114  pm2.21i  115  modal-b  2127  sbcbr123  4636  elimasni  5411  ndmfvrcl  6129  brabv  6597  oprssdm  6713  ndmovrcl  6718  omelon2  6969  omopthi  7624  fsuppres  8183  sdomsdomcardi  8680  alephgeom  8788  pwcdadom  8921  rankcf  9478  adderpq  9657  mulerpq  9658  ssnn0fi  12646  sadcp1  15015  setcepi  16561  oduclatb  16967  cntzrcl  17583  pmtrfrn  17701  dprddomcld  18223  dprdsubg  18246  psrbagsn  19316  dsmmbas2  19900  dsmmfi  19901  istps  20551  isusp  21875  dscmet  22187  dscopn  22188  i1f1lem  23262  sqff1o  24708  upgrfi  25758  umgrafi  25851  usgraedgrnv  25906  nbgranself2  25965  wwlknndef  26265  clwwlknndef  26301  dmadjrnb  28149  axpowprim  30835  opelco3  30923  sltintdifex  31060  bj-modal5e  31825  bj-modal4e  31892  topdifinffinlem  32371  finxp1o  32405  ax6fromc10  33199  axc711to11  33220  axc5c711to11  33224  pw2f1ocnv  36622  kelac1  36651  relintabex  36906  axc5c4c711toc5  37625  axc5c4c711to11  37628  disjrnmpt2  38370  afvvdm  39870  afvvfunressn  39872  afvvv  39874  afvfv0bi  39881  wwlksnndef  41111  clwwlksnndef  41198