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  1754  rb-ax3  1755  rb-ax4  1756  spimfw  1966  hba1w  2050  hbe1a  2149  sp  2190  axc4  2326  exmoeu  2581  necon1bi  2960  fvrn0  6862  nfunsn  6873  mpoxneldm  8154  mpoxopxnop0  8157  ixpprc  8857  fineqv  9167  unbndrank  9754  pf1rcl  22293  stri  32332  hstri  32340  ddemeas  34393  hbntg  35997  bj-modalb  36917  hba1-o  39153  axc5c711  39174  naecoms-o  39183  axc5c4c711  44638  hbntal  44790  resinsnlem  49112