Theorem con4i 114

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

Remark: this can also be proved using notnot 142 followed by nsyl2 141, 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  141  19.8aw  2051  modal-b  2318  euae  2653  sbcbr123  5149  brabv  5513  elimasni  6046  ndmfvrcl  6860  oprssdm  7534  ndmovrcl  7539  omelon2  7819  omopthi  8586  fsetexb  8798  fsuppres  9302  sdomsdomcardi  9886  alephgeom  9995  rankcf  10690  adderpq  10869  mulerpq  10870  ssnn0fi  13910  sadcp1  16384  setcepi  18013  oduclatb  18431  cntzrcl  19224  pmtrfrn  19355  dprddomcld  19900  dprdsubg  19923  dsmmfi  21663  psrbagsn  21986  istps  22837  isusp  24165  dscmet  24476  dscopn  24477  i1f1lem  25606  sqff1o  27108  sltintdifex  27589  nolesgn2ores  27600  nogesgn1ores  27602  nosepdmlem  27611  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  upgrfi  29054  wwlksnndef  29868  dmadjrnb  31868  antnestlaw1  35666  antnestlaw2  35667  antnestlaw3  35668  axpowprim  35679  opelco3  35750  bj-modal4e  36691  bj-snmooreb  37090  topdifinffinlem  37323  finxp1o  37368  ax6fromc10  38877  axc711to11  38898  axc5c711to11  38902  dffltz  42610  pw2f1ocnv  43013  kelac1  43039  relintabex  43557  axc5c4c711toc5  44378  axc5c4c711to11  44381  dfbi1ALTa  44916  simprimi  44917  disjrnmpt2  45169  eubrv  47023  afvvdm  47129  afvvfunressn  47131  afvvv  47133  afvfv0bi  47140  dfatafv2rnb  47215  afv20defat  47220  fafv2elrnb  47223  afv2fv0  47253