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  884  pm3.13  991  rb-ax2  1757  rb-ax3  1758  rb-ax4  1759  spimfw  1970  hba1w  2051  hbe1a  2142  sp  2178  axc4  2319  exmoeu  2581  necon1bi  2971  fvrn0  6784  nfunsn  6793  mpoxneldm  7999  mpoxopxnop0  8002  ixpprc  8665  fineqv  8967  unbndrank  9531  pf1rcl  21425  stri  30520  hstri  30528  ddemeas  32104  hbntg  33687  bj-modalb  34825  hba1-o  36838  axc5c711  36859  naecoms-o  36868  axc5c4c711  41908  hbntal  42062