Theorem con1i 149

Description: A contraposition inference. Inference associated with con1 148. 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 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con1i.1	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	1, 2	nsyl2 143	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  153  nsyl4  161  nsyl5  162  impi  167  simplim  170  nbior  885  pm3.13  992  rb-ax2  1755  rb-ax3  1756  rb-ax4  1757  spimfw  1968  hba1w  2054  hbe1a  2145  sp  2180  axc4  2329  exmoeu  2641  necon1bi  3015  fvrn0  6673  nfunsn  6682  mpoxneldm  7861  mpoxopxnop0  7864  ixpprc  8466  fineqv  8717  unbndrank  9255  pf1rcl  20973  stri  30040  hstri  30048  ddemeas  31605  hbntg  33163  bj-modalb  34163  hba1-o  36193  axc5c711  36214  naecoms-o  36223  axc5c4c711  41105  hbntal  41259