Theorem con1i 148

Description: A contraposition inference. Inference associated with con1 147. Its associated inference is mt3 204. (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 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con1i.1	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	1, 2	nsyl2 142	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  151  nsyl4  159  nsyl5  160  impi  165  simplim  168  nbior  900  pm3.13  1010  rb-ax2  1776  rb-ax3  1777  rb-ax4  1778  spimfw  1988  hba1w  2072  hbe1a  2181  sp  2221  axc4  2356  exmoeu  2611  necon1bi  2988  fvrn0  6899  nfunsn  6910  mpoxneldm  8196  mpoxopxnop0  8199  ixpprc  8905  fineqv  9215  unbndrank  9802  pf1rcl  22470  stri  32518  hstri  32526  ddemeas  34543  hbntg  36166  bj-modalb  37205  hba1-o  39533  axc5c711  39554  naecoms-o  39563  axc5c4c711  44975  hbntal  45127  resinsnlem  49500