Theorem pm2.21i 655

Description: A contradiction implies anything. Inference from pm2.21 626. (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 626	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-in2 624

This theorem is used by:  pm2.24ii  656  2false  713  pm3.2ni  825  falim  1416  pclem6  1423  dcfromcon  1498  nfnth  1518  alnex  1552  ax4sp1  1586  rex0  3539  0ss  3561  abf  3570  ral0  3629  rabsnifsb  3777  int0  3984  relndmfv  5728  nnsucelsuc  6764  nnmordi  6789  nnaordex  6801  0er  6841  fiintim  7238  indval0  9299  elnnnn0b  9611  xltnegi  10247  xnn0xadd0  10279  frec2uzltd  10853  hashf1lem2  11300  sum0  12171  fsum2dlemstep  12217  prod0  12368  fprod2dlemstep  12405  nn0enne  12685  exprmfct  12933  prm23lt5  13062  4sqlem18  13207  prmlem1a  13241  prmlem2  13254  0met  15534  ppiublem1  16210  ppiublem2  16211  lgsdir2lem3  16268  gausslemma2dlem0i  16295  2lgs  16342  2lgsoddprmlem3  16349  vtxdg0v  16654  clwwlkn0  16768  clwwlk0on0  16791