Theorem pm2.21i 641

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

This theorem is referenced by:  pm2.24ii  642  2false  696  pm3.2ni  808  falim  1362  pclem6  1369  nfnth  1458  alnex  1492  ax4sp1  1526  rex0  3432  0ss  3453  abf  3458  ral0  3516  int0  3845  nnsucelsuc  6470  nnmordi  6495  nnaordex  6507  0er  6547  fiintim  6906  elnnnn0b  9179  xltnegi  9792  xnn0xadd0  9824  frec2uzltd  10359  sum0  11351  fsum2dlemstep  11397  prod0  11548  fprod2dlemstep  11585  nn0enne  11861  exprmfct  12092  prm23lt5  12217  0met  13178  lgsdir2lem3  13725