Theorem pm2.21i 80

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

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24ii 83  bianfi 749  rex0 2343  0ss 2353  rzal 2407  ral0 2410  snsssn 2532  int0 2601  axnul2 2763  ax16b 2805  dtrucor 2829  po0 2905  so0 2921  fr0 2984  omordi 4255  omsmolem 4314  pssnn 4599  fiint 4620  alephordi 4939  nd1 5003  nd2 5004  nnsubi 6017  elioo3g 6405  elfz2 6498  om2uzlti 6556  dscmet 8003  elioo1t3 10590  hmeogrp 10632  top2usne 10643  0ded 10772  0cat 10773

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

Copyright terms: Public domain