Theorem con4bid 523

Description: A contraposition deduction.

Hypothesis

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

Assertion

Ref	Expression
con4bid	|- (ph -> (ps <-> ch))

Proof of Theorem con4bid

Step	Hyp	Ref	Expression
1		con4bid.1	. 2 |- (ph -> (-. ps <-> -. ch))
2		pm4.11 521	. 2 |- ((ps <-> ch) <-> (-. ps <-> -. ch))
3	1, 2	sylibr 200	1 |- (ph -> (ps <-> ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  pm5.21 676  necon4abid 1628  opeqex 2795  rankr1a 4664  ltaddsubt 5619  leaddsubt 5621  lt2msq 5843  supxrbnd1 6056  supxrbnd2 6057  flltt 6196  ioo0t 6323  fznt 6443  elcls 7683  chrelat3t 10289

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain