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  2054  modal-b  2325  euae  2661  sbcbr123  5154  brabv  5522  elimasni  6058  ndmfvrcl  6875  oprssdm  7549  ndmovrcl  7554  omelon2  7831  omopthi  8599  fsetexb  8813  fsuppres  9308  sdomsdomcardi  9895  alephgeom  10004  rankcf  10700  adderpq  10879  mulerpq  10880  ssnn0fi  13920  sadcp1  16394  setcepi  18024  oduclatb  18442  chnfibg  18571  cntzrcl  19268  pmtrfrn  19399  dprddomcld  19944  dprdsubg  19967  dsmmfi  21705  psrbagsn  22030  istps  22890  isusp  24217  dscmet  24528  dscopn  24529  i1f1lem  25658  sqff1o  27160  ltsintdifex  27641  nolesgn2ores  27652  nogesgn1ores  27654  nosepdmlem  27663  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  upgrfi  29176  wwlksnndef  29990  dmadjrnb  31993  antnestlaw1  35904  antnestlaw2  35905  antnestlaw3  35906  axpowprim  35917  opelco3  35988  bj-modal4e  36957  bj-snmooreb  37364  topdifinffinlem  37599  finxp1o  37644  ax6fromc10  39269  axc711to11  39290  axc5c711to11  39294  dffltz  42989  pw2f1ocnv  43391  kelac1  43417  relintabex  43934  axc5c4c711toc5  44755  axc5c4c711to11  44758  dfbi1ALTa  45292  simprimi  45293  disjrnmpt2  45544  eubrv  47392  afvvdm  47498  afvvfunressn  47500  afvvv  47502  afvfv0bi  47509  dfatafv2rnb  47584  afv20defat  47589  fafv2elrnb  47592  afv2fv0  47622