Theorem con1i 148

Description: A contraposition inference. Inference associated with con1 147. Its associated inference is mt3 204. (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 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con1i.1	. 2 ⊢ (¬ 𝜑 → 𝜓)
3	1, 2	nsyl2 142	1 ⊢ (¬ 𝜓 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.24i  151  nsyl4  159  nsyl5  160  impi  165  simplim  168  nbior  900  pm3.13  1010  rb-ax2  1783  rb-ax3  1784  rb-ax4  1785  spimfw  1995  hba1w  2079  hbe1a  2179  sp  2219  axc4  2354  exmoeu  2609  necon1bi  2986  fvrn0  6909  nfunsn  6920  mpoxneldm  8204  mpoxopxnop0  8207  ixpprc  8913  fineqv  9223  unbndrank  9810  pf1rcl  22518  stri  32618  hstri  32626  ddemeas  34635  hbntg  36303  bj-modalb  37371  hba1-o  39699  axc5c711  39720  naecoms-o  39729  axc5c4c711  45139  hbntal  45290  resinsnlem  49677