Theorem con1i 146

Description: A contraposition inference. Inference associated with con1 145. Its associated inference is mt3 192. (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 144	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  147  nsyl4  157  impi  161  simplim  164  nbior  866  pm5.55  925  pm3.13  969  rb-ax2  1826  rb-ax3  1827  rb-ax4  1828  spimfw  2047  hba1w  2131  hba1wOLD  2132  hbe1a  2177  sp  2207  axc4  2294  exmoeu  2651  moanim  2678  moexex  2690  necon1bi  2971  fvrn0  6358  nfunsn  6367  mpt2xneldm  7491  mpt2xopxnop0  7494  ixpprc  8084  fineqv  8332  unbndrank  8870  pf1rcl  19929  stri  29457  hstri  29465  ddemeas  30640  hbntg  32048  bj-modalb  33044  hba1-o  34706  axc5c711  34727  naecoms-o  34736  axc5c4c711  39129  hbntal  39295