Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 202. (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  893  pm3.13  1002  rb-ax2  1760  rb-ax3  1761  rb-ax4  1762  spimfw  1972  hba1w  2056  hbe1a  2155  sp  2195  axc4  2330  exmoeu  2585  necon1bi  2963  fvrn0  6862  nfunsn  6873  mpoxneldm  8159  mpoxopxnop0  8162  ixpprc  8864  fineqv  9174  unbndrank  9764  pf1rcl  22342  stri  32353  hstri  32361  ddemeas  34427  hbntg  36038  bj-modalb  37068  hba1-o  39396  axc5c711  39417  naecoms-o  39426  axc5c4c711  44852  hbntal  45004  resinsnlem  49368