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 735  rex0 2281  0ss 2291  rzal 2345  ral0 2348  snsssn 2469  int0 2537  axnul2 2698  ax16b 2739  dtrucor 2763  po0 2840  so0 2856  fr0 2917  omordi 4181  omsmolem 4240  pssnn 4513  fiint 4534  alephordi 4846  nd1 4910  nd2 4911  nnsub 5903  om2uzlt 6235  elioo3g 6317  elfz2t 6404  dscmet 7856  elioo1t3 10383  hmeogrp 10425  0ded 10534  0cat 10535

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

Copyright terms: Public domain