Theorem bicon2d 404

Description: A contraposition deduction.

Hypothesis

Ref	Expression
bicon2d.1	⊢ (φ → (ψ ↔ ¬ χ))

Assertion

Ref	Expression
bicon2d	⊢ (φ → (χ ↔ ¬ ψ))

Proof of Theorem bicon2d

Step	Hyp	Ref	Expression
1		bicon2d.1	. 2 ⊢ (φ → (ψ ↔ ¬ χ))
2		bicon2 403	. 2 ⊢ ((χ ↔ ¬ ψ) ↔ (ψ ↔ ¬ χ))
3	1, 2	sylibr 175	1 ⊢ (φ → (χ ↔ ¬ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127

This theorem is referenced by:  bicon1d 405  r19.9rzv 1768  sotric 2148  sotrieq 2149  so 2152  ordtri2 2233  ord0eln0 2278  limsssuc 2362  nlimon 2369  oawordeulem 3156  onomeneq 3414  rankr1 3518  ondomcard 3663  prlem934b 3932  suplem2pr 3956  sqgt0sr 4009  suppsr2 4017  suppsr3 4018  leloet 4284  leltnet 4287  lt1nnn 4442  nn0ltp1let 4556  elnnz1 4581  zltp1let 4597  uzwo 4605  nnwoOLD 4608  om2uzf1o 4656  znnenlem 4929  znnen 4930  infxpidmlem10 4942

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org