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  3465  0ss  3486  abf  3491  ral0  3549  int0  3885  nnsucelsuc  6546  nnmordi  6571  nnaordex  6583  0er  6623  fiintim  6987  elnnnn0b  9287  xltnegi  9904  xnn0xadd0  9936  frec2uzltd  10477  sum0  11534  fsum2dlemstep  11580  prod0  11731  fprod2dlemstep  11768  nn0enne  12046  exprmfct  12279  prm23lt5  12404  4sqlem18  12549  0met  14563  lgsdir2lem3  15187  gausslemma2dlem0i  15214  2lgs  15261  2lgsoddprmlem3  15268