Theorem bitr2d 529

Description: Deduction form of bitr2 174.

Hypotheses

Ref	Expression
bitr2d.1	|- (ph -> (ps <-> ch))
bitr2d.2	|- (ph -> (ch <-> th))

Assertion

Ref	Expression
bitr2d	|- (ph -> (th <-> ps))

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 |- (ph -> (ps <-> ch))
2		bitr2d.2	. . 3 |- (ph -> (ch <-> th))
3	1, 2	bitrd 528	. 2 |- (ph -> (ps <-> th))
4	3	bicomd 521	1 |- (ph -> (th <-> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3bitrrd 545  3bitr2rd 547  sbccomglem 1988  2ndconst 4097  ltxrltt 5500  posdift 5654  subge0t 5674  ltdivmult 5867  ltdivmultOLD 5868  ledivmultOLD 5869  nnleltp1t 5954  nn0subt 6161  zlem1ltt 6183  zltlem1t 6184  ioon0t 6369  fzrev2t 6512  fz1sbct 6517  sqrle 6707  sqrlt 6708  dsupivthlem 7291  znnen 7502  metcnp3 7896  bl2ioo 7911  iscauf 7939  minveclem28 8572  sinperlem2 8687  hial2eq2t 8973  pjspansnt 9500  adjsymt 9759  cnvadj 9816  eigvalclt 9885  mddmdt 10228  mdslmd2 10257  elat2 10267

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