Theorem con1i 149

Description: A contraposition inference. Inference associated with con1 148. Its associated inference is mt3 203. (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  impi  166  simplim  169  nbior  884  pm5.55  945  pm3.13  991  rb-ax2  1754  rb-ax3  1755  rb-ax4  1756  spimfw  1968  hba1w  2054  hbe1a  2148  sp  2182  axc4  2340  exmoeu  2666  moanimlem  2703  moexexlem  2711  necon1bi  3044  fvrn0  6698  nfunsn  6707  mpoxneldm  7878  mpoxopxnop0  7881  ixpprc  8483  fineqv  8733  unbndrank  9271  pf1rcl  20512  stri  30034  hstri  30042  ddemeas  31495  hbntg  33050  bj-modalb  34050  wl-nax6im  34773  hba1-o  36048  axc5c711  36069  naecoms-o  36078  axc5c4c711  40782  hbntal  40936