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  1786  rb-ax3  1787  rb-ax4  1788  spimfw  1998  hba1w  2082  hbe1a  2181  sp  2221  axc4  2353  exmoeu  2608  necon1bi  2985  fvrn0  6910  nfunsn  6921  mpoxneldm  8214  mpoxopxnop0  8217  ixpprc  8930  fineqv  9241  unbndrank  9828  pf1rcl  22580  stri  32746  hstri  32754  ddemeas  34755  hbntg  36390  bj-modalb  37459  hba1-o  39778  axc5c711  39799  naecoms-o  39808  axc5c4c711  45233  hbntal  45384  resinsnlem  49805