Theorem con1i 136

Description: A contraposition inference. Inference associated with con1 135. Its associated inference is mt3 187. (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 134	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  140  nsyl4  151  impi  155  simplim  158  pm3.13  515  nbior  891  pm5.55  927  rb-ax2  1666  rb-ax3  1667  rb-ax4  1668  spimfw  1826  hba1w  1922  sp  1990  axc4  1991  exmoeu  2385  moanim  2412  moexex  2424  necon1bi  2705  fvrn0  5950  nfunsn  5959  mpt2xneldm  7036  mpt2xopxnop0  7039  ixpprc  7626  fineqv  7871  unbndrank  8398  pf1rcl  19095  wlkntrllem3  25452  stri  28073  hstri  28081  ddemeas  29213  hbntg  30603  bj-modalb  31494  bj-naecomsv  31537  wl-dveeq12  32088  hba1-o  32702  axc5c711  32722  naecoms-o  32731  axc5c4c711  37109  hbntal  37276