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  2311  euae  2659  sbcbr123  5135  brabv  5495  elimasni  6009  ndmfvrcl  6837  oprssdm  7485  ndmovrcl  7490  omelon2  7757  omopthi  8522  fsetexb  8683  fsuppres  9201  sdomsdomcardi  9777  alephgeom  9888  rankcf  10583  adderpq  10762  mulerpq  10763  ssnn0fi  13755  sadcp1  16211  setcepi  17852  oduclatb  18274  cntzrcl  18982  pmtrfrn  19115  dprddomcld  19653  dprdsubg  19676  dsmmfi  20994  psrbagsn  21320  istps  22132  isusp  23462  dscmet  23777  dscopn  23778  i1f1lem  24902  sqff1o  26380  upgrfi  27510  wwlksnndef  28319  dmadjrnb  30317  axpowprim  33694  opelco3  33798  sltintdifex  33913  nolesgn2ores  33924  nogesgn1ores  33926  nosepdmlem  33935  nosupbnd1lem3  33962  nosupbnd1lem5  33964  nosupbnd2lem1  33967  noinfbnd1lem3  33977  noinfbnd1lem5  33979  noinfbnd2lem1  33982  bj-modal4e  34946  bj-snmooreb  35333  topdifinffinlem  35566  finxp1o  35611  ax6fromc10  37110  axc711to11  37131  axc5c711to11  37135  dffltz  40666  pw2f1ocnv  41055  kelac1  41084  relintabex  41402  axc5c4c711toc5  42233  axc5c4c711to11  42236  disjrnmpt2  42946  eubrv  44773  afvvdm  44877  afvvfunressn  44879  afvvv  44881  afvfv0bi  44888  dfatafv2rnb  44963  afv20defat  44968  fafv2elrnb  44971  afv2fv0  45001