Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (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  885  pm3.13  992  rb-ax2  1756  rb-ax3  1757  rb-ax4  1758  spimfw  1969  hba1w  2050  hbe1a  2140  sp  2176  axc4  2315  exmoeu  2581  necon1bi  2972  fvrn0  6802  nfunsn  6811  mpoxneldm  8028  mpoxopxnop0  8031  ixpprc  8707  fineqv  9038  unbndrank  9600  pf1rcl  21515  stri  30619  hstri  30627  ddemeas  32204  hbntg  33781  bj-modalb  34898  hba1-o  36911  axc5c711  36932  naecoms-o  36941  axc5c4c711  42019  hbntal  42173