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	con4i 74	1 |- (ph -> ps)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24ii 80  bianfi 742  rex0 2344  0ss 2354  rzal 2409  ral0 2412  snsssn 2543  int0 2614  axnul2 2782  ax16b 2832  dtrucor 2849  po0 2927  so0 2944  fr0 2956  omordi 4333  omsmolem 4396  pssnn 4681  fiint 4703  alephordi 5024  nd1 5092  nd2 5093  nnsubi 6102  elioo3g 6506  elfz2 6600  om2uzlti 6661  dscmet 8129  elioo1t3 10996  hmeogrp 11044  top2usne 11051  altretop 11144  0ded 11211  0cat 11212  r19.2zb 11393  fimax 11837  heiborlem42 12052

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

Copyright terms: Public domain