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  2087  modal-b  2353  euae  2687  sbcbr123  5166  brabv  5548  elimasni  6107  ndmfvrcl  6949  oprssdm  7634  ndmovrcl  7639  omelon2  7924  omopthi  8708  fsetexb  8924  fsuppres  9422  sdomsdomcardi  10089  alephgeom  10200  rankcf  10901  adderpq  11080  mulerpq  11081  ssnn0fi  14168  sadcp1  16669  setcepi  18313  oduclatb  18731  chnfibg  18860  cntzrcl  19592  pmtrfrn  19723  dprddomcld  20268  dprdsubg  20291  dsmmfi  22099  psrbagsn  22427  istps  23307  isusp  24635  dscmet  24946  dscopn  24947  i1f1lem  26065  sqff1o  27566  ltsintdifex  28075  nolesgn2ores  28086  nogesgn1ores  28088  nosepdmlem  28097  nosupbnd1lem3  28124  nosupbnd1lem5  28126  nosupbnd2lem1  28129  noinfbnd1lem3  28139  noinfbnd1lem5  28141  noinfbnd2lem1  28144  upgrfi  29726  wwlksnndef  30551  dmadjrnb  32565  jltaleph  36067  antnestlaw1  36664  antnestlaw2  36665  antnestlaw3  36666  axpowprim  36684  opelco3  36754  bj-modal4e  37834  bj-snmooreb  38305  topdifinffinlem  38538  finxp1o  38583  ax6fromc10  40219  axc711to11  40240  axc5c711to11  40244  dffltz  43936  pw2f1ocnv  44310  kelac1  44331  relintabex  44843  axc5c4c711toc5  45647  axc5c4c711to11  45650  dfbi1ALTa  46193  simprimi  46194  disjrnmpt2  46476  eubrv  48378  afvvdm  48484  afvvfunressn  48486  afvvv  48488  afvfv0bi  48495  dfatafv2rnb  48570  afv20defat  48575  fafv2elrnb  48578  afv2fv0  48608