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  3441  0ss  3462  abf  3467  ral0  3525  int0  3859  nnsucelsuc  6492  nnmordi  6517  nnaordex  6529  0er  6569  fiintim  6928  elnnnn0b  9220  xltnegi  9835  xnn0xadd0  9867  frec2uzltd  10403  sum0  11396  fsum2dlemstep  11442  prod0  11593  fprod2dlemstep  11630  nn0enne  11907  exprmfct  12138  prm23lt5  12263  0met  13887  lgsdir2lem3  14434  2lgsoddprmlem3  14462