Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (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  994  rb-ax2  1756  rb-ax3  1757  rb-ax4  1758  spimfw  1970  hba1w  2051  hbe1a  2141  sp  2177  axc4  2315  exmoeu  2576  necon1bi  2970  fvrn0  6922  nfunsn  6934  mpoxneldm  8197  mpoxopxnop0  8200  ixpprc  8913  fineqv  9263  unbndrank  9837  pf1rcl  21868  stri  31510  hstri  31518  ddemeas  33234  hbntg  34777  bj-modalb  35594  hba1-o  37767  axc5c711  37788  naecoms-o  37797  axc5c4c711  43160  hbntal  43314