Theorem con1i 147

Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 203. (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  898  pm3.13  1007  rb-ax2  1772  rb-ax3  1773  rb-ax4  1774  spimfw  1984  hba1w  2068  hbe1a  2177  sp  2217  axc4  2352  exmoeu  2607  necon1bi  2984  fvrn0  6891  nfunsn  6902  mpoxneldm  8187  mpoxopxnop0  8190  ixpprc  8897  fineqv  9207  unbndrank  9797  pf1rcl  22392  stri  32406  hstri  32414  ddemeas  34494  hbntg  36117  bj-modalb  37157  hba1-o  39485  axc5c711  39506  naecoms-o  39515  axc5c4c711  44941  hbntal  45093  resinsnlem  49456