Theorem pm2.21i 647

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

This theorem is referenced by:  pm2.24ii  648  2false  703  pm3.2ni  815  falim  1387  pclem6  1394  dcfromcon  1469  nfnth  1489  alnex  1523  ax4sp1  1557  rex0  3479  0ss  3500  abf  3505  ral0  3563  int0  3901  nnsucelsuc  6584  nnmordi  6609  nnaordex  6621  0er  6661  fiintim  7035  elnnnn0b  9346  xltnegi  9964  xnn0xadd0  9996  frec2uzltd  10555  sum0  11743  fsum2dlemstep  11789  prod0  11940  fprod2dlemstep  11977  nn0enne  12257  exprmfct  12504  prm23lt5  12630  4sqlem18  12775  0met  14900  lgsdir2lem3  15551  gausslemma2dlem0i  15578  2lgs  15625  2lgsoddprmlem3  15632