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  3528  0ss  3549  abf  3554  ral0  3613  rabsnifsb  3759  int0  3965  nnsucelsuc  6726  nnmordi  6751  nnaordex  6763  0er  6803  fiintim  7193  elnnnn0b  9545  xltnegi  10174  xnn0xadd0  10206  frec2uzltd  10772  sum0  12082  fsum2dlemstep  12128  prod0  12279  fprod2dlemstep  12316  nn0enne  12596  exprmfct  12843  prm23lt5  12969  4sqlem18  13114  0met  15298  lgsdir2lem3  15952  gausslemma2dlem0i  15979  2lgs  16026  2lgsoddprmlem3  16033  vtxdg0v  16338  clwwlkn0  16452  clwwlk0on0  16475