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  2050  modal-b  2319  euae  2659  sbcbr123  5173  brabv  5543  elimasni  6078  ndmfvrcl  6912  oprssdm  7588  ndmovrcl  7593  omelon2  7874  omopthi  8673  fsetexb  8878  fsuppres  9405  sdomsdomcardi  9985  alephgeom  10096  rankcf  10791  adderpq  10970  mulerpq  10971  ssnn0fi  14003  sadcp1  16474  setcepi  18101  oduclatb  18517  cntzrcl  19310  pmtrfrn  19439  dprddomcld  19984  dprdsubg  20007  dsmmfi  21698  psrbagsn  22021  istps  22872  isusp  24200  dscmet  24511  dscopn  24512  i1f1lem  25642  sqff1o  27144  sltintdifex  27625  nolesgn2ores  27636  nogesgn1ores  27638  nosepdmlem  27647  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  upgrfi  29070  wwlksnndef  29887  dmadjrnb  31887  axpowprim  35721  opelco3  35792  bj-modal4e  36733  bj-snmooreb  37132  topdifinffinlem  37365  finxp1o  37410  ax6fromc10  38914  axc711to11  38935  axc5c711to11  38939  dffltz  42657  pw2f1ocnv  43061  kelac1  43087  relintabex  43605  axc5c4c711toc5  44426  axc5c4c711to11  44429  dfbi1ALTa  44964  simprimi  44965  disjrnmpt2  45212  eubrv  47064  afvvdm  47170  afvvfunressn  47172  afvvv  47174  afvfv0bi  47181  dfatafv2rnb  47256  afv20defat  47261  fafv2elrnb  47264  afv2fv0  47294