Theorem pm2.21i 646

Description: A contradiction implies anything. Inference from pm2.21 617. (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 617	. 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 615

This theorem is referenced by:  pm2.24ii  647  2false  701  pm3.2ni  813  falim  1367  pclem6  1374  nfnth  1465  alnex  1499  ax4sp1  1533  rex0  3440  0ss  3461  abf  3466  ral0  3524  int0  3857  nnsucelsuc  6487  nnmordi  6512  nnaordex  6524  0er  6564  fiintim  6923  elnnnn0b  9214  xltnegi  9829  xnn0xadd0  9861  frec2uzltd  10396  sum0  11387  fsum2dlemstep  11433  prod0  11584  fprod2dlemstep  11621  nn0enne  11897  exprmfct  12128  prm23lt5  12253  0met  13666  lgsdir2lem3  14213