Theorem con4i 114

Description: Inference associated with con4 113. Its associated inference is mt4 116.

Remark: this can also be proved using notnot 144 followed by nsyl2 143, 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 113	. 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  116  pm2.21i  119  nsyl2  143  modal-b  2338  euae  2745  sbcbr123  5120  brabv  5453  elimasni  5956  ndmfvrcl  6701  oprssdm  7329  ndmovrcl  7334  omelon2  7592  omopthi  8284  fsuppres  8858  sdomsdomcardi  9400  alephgeom  9508  rankcf  10199  adderpq  10378  mulerpq  10379  ssnn0fi  13354  sadcp1  15804  setcepi  17348  oduclatb  17754  cntzrcl  18457  pmtrfrn  18586  dprddomcld  19123  dprdsubg  19146  psrbagsn  20275  dsmmfi  20882  istps  21542  isusp  22870  dscmet  23182  dscopn  23183  i1f1lem  24290  sqff1o  25759  upgrfi  26876  wwlksnndef  27683  dmadjrnb  29683  axpowprim  32930  opelco3  33018  sltintdifex  33168  nolesgn2ores  33179  nosepdmlem  33187  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  bj-modal4e  34049  bj-snmooreb  34409  topdifinffinlem  34631  finxp1o  34676  ax6fromc10  36047  axc711to11  36068  axc5c711to11  36072  dffltz  39291  pw2f1ocnv  39654  kelac1  39683  relintabex  39961  axc5c4c711toc5  40754  axc5c4c711to11  40757  disjrnmpt2  41469  eubrv  43290  afvvdm  43360  afvvfunressn  43362  afvvv  43364  afvfv0bi  43371  dfatafv2rnb  43446  afv20defat  43451  fafv2elrnb  43454  afv2fv0  43484