Theorem con2d 91

Description: A contraposition deduction.

Hypothesis

Ref	Expression
con2d.1	|- (ph -> (ps -> -. ch))

Assertion

Ref	Expression
con2d	|- (ph -> (ch -> -. ps))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		con2d.1	. 2 |- (ph -> (ps -> -. ch))
2		con2 90	. 2 |- ((ps -> -. ch) -> (ch -> -. ps))
3	1, 2	syl 10	1 |- (ph -> (ch -> -. ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  con3 94  mt2i 110  mt2d 111  pm3.2im 122  pm2.65 134  pm3.37 286  necon2ad 1606  necon2bd 1607  cla4egf 1852  minel 2314  sotric 2851  onnminsb 3006  oneqmin 3008  onminex 3010  ordunisuc2 3105  limsssuc 3111  funun 3540  imadif 3560  tz7.48lem 3940  pssinf 4507  unblem1 4517  supnub 4556  elirrv 4570  inf3lem6 4590  cardne 4802  carddom 4808  ondomcard 4829  cardmin 4832  alephnbtwn 4840  addnidpi 5000  genpnnp 5080  lt0nnn0 6063  nn0ge0t 6064  btwnnzt 6139  primet 6142  qsqueeze 6218  ivthlem6 7221  ivthlem6OLD 7230  elcls 7646  normgt0tOLD 8914  stadd3 10085  cvnsymt 10127  cvntrt 10129  atcvat 10221

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

Copyright terms: Public domain