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  887  pm3.13  996  rb-ax2  1752  rb-ax3  1753  rb-ax4  1754  spimfw  1964  hba1w  2046  hbe1a  2143  sp  2182  axc4  2320  exmoeu  2580  necon1bi  2968  fvrn0  6935  nfunsn  6947  mpoxneldm  8238  mpoxopxnop0  8241  ixpprc  8960  fineqv  9300  unbndrank  9883  pf1rcl  22354  stri  32277  hstri  32285  ddemeas  34238  hbntg  35807  bj-modalb  36718  hba1-o  38899  axc5c711  38920  naecoms-o  38929  axc5c4c711  44425  hbntal  44578  resinsnlem  48777