Theorem pm2.21i 77

Description: A contradiction implies anything. Inference from pm2.21 76.

Hypothesis

Ref	Expression
pm2.21i.1	|- -. ph

Assertion

Ref	Expression
pm2.21i	|- (ph -> ps)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 |- -. ph
2	1	a1i 8	. 2 |- (-. ps -> -. ph)
3	2	a3i 74	1 |- (ph -> ps)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24ii 80  bianfi 739  rex0 2295  0ss 2305  rzal 2359  ral0 2362  snsssn 2482  int0 2551  axnul2 2713  ax16b 2755  dtrucor 2779  po0 2855  so0 2871  fr0 2933  omordi 4203  omsmolem 4262  pssnn 4544  fiint 4572  fiintOLD 4573  alephordi 4885  nd1 4950  nd2 4951  nnsub 5958  om2uzlt 6299  elioo3g 6381  elfz2t 6473  dscmet 7915  elioo1t3 10482  hmeogrp 10524  top2usne 10535  0ded 10661  0cat 10662

This theorem was proved from axioms:  ax-1 4  ax-3 6  ax-mp 7

Copyright terms: Public domain