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  708  pm3.2ni  820  falim  1411  pclem6  1418  dcfromcon  1493  nfnth  1513  alnex  1547  ax4sp1  1581  rex0  3512  0ss  3533  abf  3538  ral0  3596  rabsnifsb  3737  int0  3942  nnsucelsuc  6659  nnmordi  6684  nnaordex  6696  0er  6736  fiintim  7123  elnnnn0b  9446  xltnegi  10070  xnn0xadd0  10102  frec2uzltd  10666  sum0  11951  fsum2dlemstep  11997  prod0  12148  fprod2dlemstep  12185  nn0enne  12465  exprmfct  12712  prm23lt5  12838  4sqlem18  12983  0met  15111  lgsdir2lem3  15762  gausslemma2dlem0i  15789  2lgs  15836  2lgsoddprmlem3  15843  vtxdg0v  16148  clwwlkn0  16262  clwwlk0on0  16285