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  2350  euae  2685  sbcbr123  5160  brabv  5541  elimasni  6089  ndmfvrcl  6919  oprssdm  7603  ndmovrcl  7608  omelon2  7891  omopthi  8671  fsetexb  8887  fsuppres  9386  sdomsdomcardi  10053  alephgeom  10162  rankcf  10863  adderpq  11042  mulerpq  11043  ssnn0fi  14129  sadcp1  16626  setcepi  18264  oduclatb  18682  chnfibg  18811  cntzrcl  19542  pmtrfrn  19673  dprddomcld  20218  dprdsubg  20241  dsmmfi  22045  psrbagsn  22373  istps  23253  isusp  24581  dscmet  24892  dscopn  24893  i1f1lem  26011  sqff1o  27510  ltsintdifex  28019  nolesgn2ores  28030  nogesgn1ores  28032  nosepdmlem  28041  nosupbnd1lem3  28068  nosupbnd1lem5  28070  nosupbnd2lem1  28073  noinfbnd1lem3  28083  noinfbnd1lem5  28085  noinfbnd2lem1  28088  upgrfi  29670  wwlksnndef  30495  dmadjrnb  32509  antnestlaw1  36457  antnestlaw2  36458  antnestlaw3  36459  axpowprim  36470  opelco3  36540  bj-modal4e  37620  bj-snmooreb  38036  topdifinffinlem  38272  finxp1o  38317  ax6fromc10  39955  axc711to11  39976  axc5c711to11  39980  dffltz  43672  pw2f1ocnv  44045  kelac1  44066  relintabex  44583  axc5c4c711toc5  45387  axc5c4c711to11  45390  dfbi1ALTa  45930  simprimi  45931  disjrnmpt2  46204  eubrv  48106  afvvdm  48212  afvvfunressn  48214  afvvv  48216  afvfv0bi  48223  dfatafv2rnb  48298  afv20defat  48303  fafv2elrnb  48306  afv2fv0  48336