Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 201. (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  888  pm3.13  997  rb-ax2  1755  rb-ax3  1756  rb-ax4  1757  spimfw  1967  hba1w  2051  hbe1a  2150  sp  2191  axc4  2327  exmoeu  2582  necon1bi  2961  fvrn0  6870  nfunsn  6881  mpoxneldm  8164  mpoxopxnop0  8167  ixpprc  8869  fineqv  9179  unbndrank  9766  pf1rcl  22305  stri  32344  hstri  32352  ddemeas  34413  hbntg  36016  bj-modalb  36955  hba1-o  39267  axc5c711  39288  naecoms-o  39297  axc5c4c711  44751  hbntal  44903  resinsnlem  49224