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  705  pm3.2ni  817  falim  1389  pclem6  1396  dcfromcon  1471  nfnth  1491  alnex  1525  ax4sp1  1559  rex0  3489  0ss  3510  abf  3515  ral0  3573  int0  3916  nnsucelsuc  6607  nnmordi  6632  nnaordex  6644  0er  6684  fiintim  7061  elnnnn0b  9381  xltnegi  9999  xnn0xadd0  10031  frec2uzltd  10592  sum0  11865  fsum2dlemstep  11911  prod0  12062  fprod2dlemstep  12099  nn0enne  12379  exprmfct  12626  prm23lt5  12752  4sqlem18  12897  0met  15023  lgsdir2lem3  15674  gausslemma2dlem0i  15701  2lgs  15748  2lgsoddprmlem3  15755