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  901  pm3.13  1010  rb-ax2  1785  rb-ax3  1786  rb-ax4  1787  spimfw  1997  hba1w  2081  hbe1a  2180  sp  2219  axc4  2351  exmoeu  2606  necon1bi  2983  fvrn0  6913  nfunsn  6924  mpoxneldm  8232  mpoxopxnop0  8235  ixpprc  8950  fineqv  9261  unbndrank  9858  pf1rcl  22672  stri  32864  hstri  32872  ddemeas  34915  hbntg  36659  bj-modalb  37712  hba1-o  40047  axc5c711  40068  naecoms-o  40077  axc5c4c711  45478  hbntal  45629  resinsnlem  50077