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  702  pm3.2ni  814  falim  1378  pclem6  1385  nfnth  1476  alnex  1510  ax4sp1  1544  rex0  3464  0ss  3485  abf  3490  ral0  3548  int0  3884  nnsucelsuc  6544  nnmordi  6569  nnaordex  6581  0er  6621  fiintim  6985  elnnnn0b  9284  xltnegi  9901  xnn0xadd0  9933  frec2uzltd  10474  sum0  11531  fsum2dlemstep  11577  prod0  11728  fprod2dlemstep  11765  nn0enne  12043  exprmfct  12276  prm23lt5  12401  4sqlem18  12546  0met  14552  lgsdir2lem3  15146  gausslemma2dlem0i  15173  2lgsoddprmlem3  15199