Theorem con4i 115

Description: Inference associated with con4 114. Its associated inference is mt4 117.

Remark: this can also be proved using notnot 143 followed by nsyl2 142, 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 114	. 2 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-3 8

This theorem is used by:  mt4  117  pm2.21i  120  nsyl2  142  19.8aw  2085  modal-b  2349  euae  2684  sbcbr123  5159  brabv  5545  elimasni  6087  ndmfvrcl  6911  oprssdm  7595  ndmovrcl  7600  omelon2  7875  omopthi  8649  fsetexb  8865  fsuppres  9363  sdomsdomcardi  9976  alephgeom  10085  rankcf  10786  adderpq  10965  mulerpq  10966  ssnn0fi  14049  sadcp1  16545  setcepi  18177  oduclatb  18595  chnfibg  18724  cntzrcl  19454  pmtrfrn  19585  dprddomcld  20130  dprdsubg  20153  dsmmfi  21951  psrbagsn  22279  istps  23159  isusp  24487  dscmet  24798  dscopn  24799  i1f1lem  25917  sqff1o  27418  ltsintdifex  27897  nolesgn2ores  27908  nogesgn1ores  27910  nosepdmlem  27919  nosupbnd1lem3  27946  nosupbnd1lem5  27948  nosupbnd2lem1  27951  noinfbnd1lem3  27961  noinfbnd1lem5  27963  noinfbnd2lem1  27966  upgrfi  29548  wwlksnndef  30373  dmadjrnb  32387  antnestlaw1  36270  antnestlaw2  36271  antnestlaw3  36272  axpowprim  36283  opelco3  36354  bj-modal4e  37450  bj-snmooreb  37864  topdifinffinlem  38101  finxp1o  38146  ax6fromc10  39769  axc711to11  39790  axc5c711to11  39794  dffltz  43480  pw2f1ocnv  43878  kelac1  43904  relintabex  44421  axc5c4c711toc5  45226  axc5c4c711to11  45229  dfbi1ALTa  45762  simprimi  45763  disjrnmpt2  46020  eubrv  47923  afvvdm  48029  afvvfunressn  48031  afvvv  48033  afvfv0bi  48040  dfatafv2rnb  48115  afv20defat  48120  fafv2elrnb  48123  afv2fv0  48153