Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 201. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)

Hypothesis

Ref	Expression
con1i.1	⊢ (¬ 𝜑 → 𝜓)

Assertion

Ref	Expression
con1i	⊢ (¬ 𝜓 → 𝜑)

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con1i.1	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	1, 2	nsyl2 141	1 ⊢ (¬ 𝜓 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.24i  150  nsyl4  158  nsyl5  159  impi  164  simplim  167  nbior  886  pm3.13  995  rb-ax2  1751  rb-ax3  1752  rb-ax4  1753  spimfw  1965  hba1w  2047  hbe1a  2144  sp  2184  axc4  2325  exmoeu  2584  necon1bi  2975  fvrn0  6950  nfunsn  6962  mpoxneldm  8253  mpoxopxnop0  8256  ixpprc  8977  fineqv  9326  unbndrank  9911  pf1rcl  22374  stri  32289  hstri  32297  ddemeas  34200  hbntg  35769  bj-modalb  36682  hba1-o  38853  axc5c711  38874  naecoms-o  38883  axc5c4c711  44370  hbntal  44524