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  886  pm3.13  993  rb-ax2  1755  rb-ax3  1756  rb-ax4  1757  spimfw  1969  hba1w  2050  hbe1a  2140  sp  2176  axc4  2314  exmoeu  2574  necon1bi  2968  fvrn0  6877  nfunsn  6889  mpoxneldm  8148  mpoxopxnop0  8151  ixpprc  8864  fineqv  9214  unbndrank  9787  pf1rcl  21752  stri  31262  hstri  31270  ddemeas  32924  hbntg  34466  bj-modalb  35257  hba1-o  37432  axc5c711  37453  naecoms-o  37462  axc5c4c711  42803  hbntal  42957