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 ⊢ (¬ 𝜓 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.24i  151  nsyl4  159  nsyl5  160  impi  165  simplim  168  nbior  901  pm3.13  1010  rb-ax2  1786  rb-ax3  1787  rb-ax4  1788  spimfw  2000  hba1w  2084  hbe1a  2183  sp  2223  axc4  2355  exmoeu  2609  necon1bi  2987  fvrn0  6936  nfunsn  6947  mpoxneldm  8257  mpoxopxnop0  8260  ixpprc  8975  fineqv  9286  unbndrank  9882  pf1rcl  22697  stri  32889  hstri  32897  ddemeas  34939  hbntg  36745  bj-modalb  37798  hba1-o  40146  axc5c711  40167  naecoms-o  40176  axc5c4c711  45577  hbntal  45727  resinsnlem  50189