Theorem pm2.21i 93

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

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24ii 96  bianfi 809  ax4sp1 1316  rex0 2888  0ss 2900  abf 2906  r19.2zb 2959  rzalOLD 2971  ral0 2974  snsssn 3148  int0 3230  axnulALT 3443  ax16b 3499  dtrucor 3518  po0OLD 3602  so0OLD 3622  fr0 3636  omordi 5245  omsmolem 5313  pssnn 5628  fiint 5650  alephordi 6022  nd1 6090  nd2 6091  nnsubi 7140  elioo3g 7547  elfz2 7642  om2uzlti 7709  dscmet 9196  bnj98 13221  dford4lem2 13860  axsltsolem1 14006  FiA 14104  bisym1 14243  unqsym1 14249  amosym1 14250  subsym1 14251  elioo1t3 14846  hmeogrp 14892  top2usne 14898  altretop 14997  0ded 15104  0cat 15105  inttarcar 15278  fimax 15746  heiborlem42 15996

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

Copyright terms: Public domain