Theorem pm2.21i 649

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

This theorem is referenced by:  pm2.24ii  650  2false  706  pm3.2ni  818  falim  1409  pclem6  1416  dcfromcon  1491  nfnth  1511  alnex  1545  ax4sp1  1579  rex0  3509  0ss  3530  abf  3535  ral0  3593  int0  3937  nnsucelsuc  6650  nnmordi  6675  nnaordex  6687  0er  6727  fiintim  7109  elnnnn0b  9429  xltnegi  10048  xnn0xadd0  10080  frec2uzltd  10642  sum0  11920  fsum2dlemstep  11966  prod0  12117  fprod2dlemstep  12154  nn0enne  12434  exprmfct  12681  prm23lt5  12807  4sqlem18  12952  0met  15079  lgsdir2lem3  15730  gausslemma2dlem0i  15757  2lgs  15804  2lgsoddprmlem3  15811  vtxdg0v  16080  clwwlkn0  16177