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  2084  modal-b  2349  euae  2684  sbcbr123  5159  brabv  5540  elimasni  6088  ndmfvrcl  6919  oprssdm  7603  ndmovrcl  7608  omelon2  7891  omopthi  8674  fsetexb  8890  fsuppres  9389  sdomsdomcardi  10056  alephgeom  10165  rankcf  10866  adderpq  11045  mulerpq  11046  ssnn0fi  14132  sadcp1  16631  setcepi  18269  oduclatb  18687  chnfibg  18816  cntzrcl  19547  pmtrfrn  19678  dprddomcld  20223  dprdsubg  20246  dsmmfi  22050  psrbagsn  22378  istps  23258  isusp  24586  dscmet  24897  dscopn  24898  i1f1lem  26016  sqff1o  27515  ltsintdifex  28024  nolesgn2ores  28035  nogesgn1ores  28037  nosepdmlem  28046  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noinfbnd2lem1  28093  upgrfi  29675  wwlksnndef  30500  dmadjrnb  32514  antnestlaw1  36543  antnestlaw2  36544  antnestlaw3  36545  axpowprim  36562  opelco3  36632  bj-modal4e  37712  bj-snmooreb  38128  topdifinffinlem  38364  finxp1o  38409  ax6fromc10  40047  axc711to11  40068  axc5c711to11  40072  dffltz  43764  pw2f1ocnv  44138  kelac1  44159  relintabex  44676  axc5c4c711toc5  45480  axc5c4c711to11  45483  dfbi1ALTa  46023  simprimi  46024  disjrnmpt2  46297  eubrv  48199  afvvdm  48305  afvvfunressn  48307  afvvv  48309  afvfv0bi  48316  dfatafv2rnb  48391  afv20defat  48396  fafv2elrnb  48399  afv2fv0  48429