Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 201. (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  996  rb-ax2  1753  rb-ax3  1754  rb-ax4  1755  spimfw  1965  hba1w  2048  hbe1a  2145  sp  2184  axc4  2320  exmoeu  2574  necon1bi  2953  fvrn0  6850  nfunsn  6862  mpoxneldm  8145  mpoxopxnop0  8148  ixpprc  8846  fineqv  9156  unbndrank  9738  pf1rcl  22234  stri  32201  hstri  32209  ddemeas  34203  hbntg  35779  bj-modalb  36690  hba1-o  38876  axc5c711  38897  naecoms-o  38906  axc5c4c711  44374  hbntal  44527  resinsnlem  48855