Theorem pm2.24i 145

Description: Inference associated with pm2.24 120. Its associated inference is pm2.24ii 116. (Contributed by NM, 20-Aug-2001.)

Hypothesis

Ref	Expression
pm2.24i.1	⊢ 𝜑

Assertion

Ref	Expression
pm2.24i	⊢ (¬ 𝜑 → 𝜓)

Proof of Theorem pm2.24i

Step	Hyp	Ref	Expression
1		pm2.24i.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (¬ 𝜓 → 𝜑)
3	2	con1i 143	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:  orci  404  niabn  989  ax13dgen1  2001  prm23ge5  15358  pmtrdifellem4  17722  usgraidx2v  25922  nbgra0nb  25958  nbgranself  25963  frgra3vlem1  26527  frgra3vlem2  26528  3vfriswmgralem  26531  negsym1  31586  usgredg2v  40454  frgr3vlem1  41443  frgr3vlem2  41444  3vfriswmgrlem  41447