Theorem pm2.21i 651

Description: A contradiction implies anything. Inference from pm2.21 622. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
pm2.21i.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
pm2.21i	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. 2 ⊢ ¬ 𝜑
2		pm2.21 622	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-in2 620

This theorem is referenced by:  pm2.24ii  652  2false  709  pm3.2ni  821  falim  1412  pclem6  1419  dcfromcon  1494  nfnth  1514  alnex  1548  ax4sp1  1582  rex0  3525  0ss  3546  abf  3551  ral0  3610  rabsnifsb  3756  int0  3962  nnsucelsuc  6723  nnmordi  6748  nnaordex  6760  0er  6800  fiintim  7190  elnnnn0b  9536  xltnegi  10164  xnn0xadd0  10196  frec2uzltd  10761  sum0  12067  fsum2dlemstep  12113  prod0  12264  fprod2dlemstep  12301  nn0enne  12581  exprmfct  12828  prm23lt5  12954  4sqlem18  13099  0met  15236  lgsdir2lem3  15890  gausslemma2dlem0i  15917  2lgs  15964  2lgsoddprmlem3  15971  vtxdg0v  16276  clwwlkn0  16390  clwwlk0on0  16413