Theorem con1i 144

Description: A contraposition inference. Inference associated with con1 143. Its associated inference is mt3 192. (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 142	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  146  nsyl4  156  impi  160  simplim  163  pm3.13  522  nbior  904  pm5.55  938  rb-ax2  1675  rb-ax3  1676  rb-ax4  1677  spimfw  1875  hba1w  1971  hba1wOLD  1972  hbe1a  2019  sp  2051  axc4  2126  exmoeu  2501  moanim  2528  moexex  2540  necon1bi  2818  fvrn0  6173  nfunsn  6182  mpt2xneldm  7283  mpt2xopxnop0  7286  ixpprc  7873  fineqv  8119  unbndrank  8649  pf1rcl  19632  stri  28965  hstri  28973  ddemeas  30080  hbntg  31412  bj-modalb  32348  hba1-o  33662  axc5c711  33683  naecoms-o  33692  axc5c4c711  38084  hbntal  38251