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  dcfromcon  1459  nfnth  1479  alnex  1513  ax4sp1  1547  rex0  3469  0ss  3490  abf  3495  ral0  3553  int0  3889  nnsucelsuc  6558  nnmordi  6583  nnaordex  6595  0er  6635  fiintim  7001  elnnnn0b  9312  xltnegi  9929  xnn0xadd0  9961  frec2uzltd  10514  sum0  11572  fsum2dlemstep  11618  prod0  11769  fprod2dlemstep  11806  nn0enne  12086  exprmfct  12333  prm23lt5  12459  4sqlem18  12604  0met  14706  lgsdir2lem3  15357  gausslemma2dlem0i  15384  2lgs  15431  2lgsoddprmlem3  15438