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  3530  0ss  3551  abf  3556  ral0  3615  rabsnifsb  3762  int0  3968  nnsucelsuc  6737  nnmordi  6762  nnaordex  6774  0er  6814  fiintim  7204  elnnnn0b  9560  xltnegi  10190  xnn0xadd0  10222  frec2uzltd  10792  sum0  12102  fsum2dlemstep  12148  prod0  12299  fprod2dlemstep  12336  nn0enne  12616  exprmfct  12863  prm23lt5  12989  4sqlem18  13134  0met  15378  lgsdir2lem3  16032  gausslemma2dlem0i  16059  2lgs  16106  2lgsoddprmlem3  16113  vtxdg0v  16418  clwwlkn0  16532  clwwlk0on0  16555