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 1614  necon2bd 1615  cla4egf 1861  minel 2324  sotric 2860  onnminsb 3016  oneqmin 3018  onminex 3020  ordunisuc2 3115  limsssuc 3121  funun 3554  imadif 3574  tz7.48lem 3955  pssinfOLD 4528  unblem1 4540  supnub 4582  elirrv 4598  inf3lem6 4618  cardne 4830  carddom 4836  ondomcard 4857  cardmin 4860  alephnbtwn 4868  addnidpi 5028  genpnnp 5108  lt0nnn0 6116  nn0ge0t 6117  btwnnzt 6192  primet 6195  qsqueeze 6280  ivthlem6 7286  elcls 7704  normgt0tOLD 8993  cvnsymt 10217  cvntrt 10219  atcvat 10313

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

Copyright terms: Public domain