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  3468  0ss  3489  abf  3494  ral0  3552  int0  3888  nnsucelsuc  6549  nnmordi  6574  nnaordex  6586  0er  6626  fiintim  6992  elnnnn0b  9293  xltnegi  9910  xnn0xadd0  9942  frec2uzltd  10495  sum0  11553  fsum2dlemstep  11599  prod0  11750  fprod2dlemstep  11787  nn0enne  12067  exprmfct  12306  prm23lt5  12432  4sqlem18  12577  0met  14620  lgsdir2lem3  15271  gausslemma2dlem0i  15298  2lgs  15345  2lgsoddprmlem3  15352