Theorem 3bitr4d 424

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula.

Hypotheses

Ref	Expression
3bitr4d.1	|- (ph -> (ps <-> ch))
3bitr4d.2	|- (ph -> (th <-> ps))
3bitr4d.3	|- (ph -> (ta <-> ch))

Assertion

Ref	Expression
3bitr4d	|- (ph -> (th <-> ta ))

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- (ph -> (th <-> ps))
2		3bitr4d.1	. . 3 |- (ph -> (ps <-> ch))
3		3bitr4d.3	. . 3 |- (ph -> (ta <-> ch))
4	2, 3	bitr4d 409	. 2 |- (ph -> (ps <-> ta ))
5	1, 4	bitrd 406	1 |- (ph -> (th <-> ta ))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  sbcom 916  sbcom2 992  ordsucelsuc 2324  ordsucsssuc 2325  ordsucun 2333  fvopab3 2868  isotr 2935  isotrALT 2936  oacan 3150  oaword 3151  brecop 3242  omsucdom 3418  finsucdom 3421  alephord3 3683  ltsopi 3810  ltexpi 3823  ltapi 3824  ltmpi 3825  1idpr 3927  addcanpr 3946  axltadd 4085  ledivt 4405  nn0subt 4587  zltp1let 4597  qbtwnre 4650  shscomt 5284  spansncol 5473  hods 5606  cvcon3t 5716  mdsymlem8 5783

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