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  887  pm3.13  996  rb-ax2  1750  rb-ax3  1751  rb-ax4  1752  spimfw  1963  hba1w  2045  hbe1a  2142  sp  2181  axc4  2320  exmoeu  2579  necon1bi  2967  fvrn0  6937  nfunsn  6949  mpoxneldm  8236  mpoxopxnop0  8239  ixpprc  8958  fineqv  9297  unbndrank  9880  pf1rcl  22369  stri  32286  hstri  32294  ddemeas  34217  hbntg  35787  bj-modalb  36699  hba1-o  38879  axc5c711  38900  naecoms-o  38909  axc5c4c711  44397  hbntal  44551