Theorem 3bitr4d 561

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 542	. 2 |- (ph -> (ps <-> ta))
5	1, 4	bitrd 539	1 |- (ph -> (th <-> ta))

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

This theorem is referenced by:  sbcom 1300  sbcom2 1376  cbvsbcv 2007  sbcralt 2040  sbcralgf 2042  sbcel12g 2062  sbceqdig 2063  ordsucelsuc 3130  ordsucsssuc 3131  ordsucun 3139  fvopab3 3834  fvimacnvALT 3866  isotr 3955  isotrALT 3956  oaword 4241  omword 4259  om00el 4265  oeword 4275  brecop 4367  xpdom2 4505  omsucdom 4587  finsucdom 4591  alephord3 4943  ltsopi 5081  ltexpi 5094  ltapi 5095  ltmpi 5096  1idpr 5198  addcanpr 5217  pre-axltadd 5354  subsub23 5441  axlttri 5568  lemul1 5890  lediv1 5909  lediv1OLD 5910  lt2mul2div 5931  lediv2 5951  avgle 6105  nn0sub 6243  zltp1le 6263  qbtwnre 6331  iooneg 6432  iccneg 6433  fzaddel 6526  fzrev 6537  cj11 6920  neiint 7804  islp2 7832  nvsubsub23 8366  nmorepnf 8515  shscom 9366  spansncol 9574  cmcm2 9642  hodsi 9784  eigposi 9845  nmoprepnf 9877  nmfnrepnf 9890  pjssposi 10183  cvcon3 10295  mdsymlem8 10421  dmdsym 10424  hmeobc 10636

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 154  df-an 232

Copyright terms: Public domain