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  2053  modal-b  2320  euae  2655  sbcbr123  5145  brabv  5506  elimasni  6040  ndmfvrcl  6855  oprssdm  7527  ndmovrcl  7532  omelon2  7809  omopthi  8576  fsetexb  8788  fsuppres  9277  sdomsdomcardi  9864  alephgeom  9973  rankcf  10668  adderpq  10847  mulerpq  10848  ssnn0fi  13892  sadcp1  16366  setcepi  17995  oduclatb  18413  chnfibg  18542  cntzrcl  19240  pmtrfrn  19371  dprddomcld  19916  dprdsubg  19939  dsmmfi  21676  psrbagsn  21999  istps  22850  isusp  24177  dscmet  24488  dscopn  24489  i1f1lem  25618  sqff1o  27120  sltintdifex  27601  nolesgn2ores  27612  nogesgn1ores  27614  nosepdmlem  27623  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2lem1  27655  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2lem1  27670  upgrfi  29070  wwlksnndef  29884  dmadjrnb  31884  antnestlaw1  35733  antnestlaw2  35734  antnestlaw3  35735  axpowprim  35746  opelco3  35817  bj-modal4e  36755  bj-snmooreb  37154  topdifinffinlem  37387  finxp1o  37432  ax6fromc10  38941  axc711to11  38962  axc5c711to11  38966  dffltz  42673  pw2f1ocnv  43076  kelac1  43102  relintabex  43620  axc5c4c711toc5  44441  axc5c4c711to11  44444  dfbi1ALTa  44978  simprimi  44979  disjrnmpt2  45231  eubrv  47072  afvvdm  47178  afvvfunressn  47180  afvvv  47182  afvfv0bi  47189  dfatafv2rnb  47264  afv20defat  47269  fafv2elrnb  47272  afv2fv0  47302