Theorem 3bitr4d 549

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

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

This theorem is referenced by:  sbcom 1256  sbcom2 1332  sbcralt 1986  sbcralgf 1988  sbcel12g 2007  sbceqdig 2008  ordsucelsuc 3068  ordsucsssuc 3069  ordsucun 3077  fvopab3 3768  fvimacnvALT 3800  isotr 3888  isotrALT 3889  oaword 4173  omword 4191  om00el 4197  oeword 4207  brecop 4296  xpdom2 4428  omsucdom 4508  finsucdom 4512  alephord3 4858  ltsopi 4996  ltexpi 5009  ltapi 5010  ltmpi 5011  1idpr 5113  addcanpr 5132  pre-axltadd 5269  subsub23t 5356  axlttri 5483  lemul1t 5796  lediv1t 5814  lt2mul2divt 5830  lediv2t 5847  avglet 5999  nn0subt 6116  zltp1let 6136  qbtwnre 6224  ioonegt 6347  iccnegt 6348  fzaddelt 6440  fzrevt 6451  cj11t 6773  neiint 7669  islp2 7697  nvsubsub23 8234  nmorepnf 8376  shscomt 9221  spansncol 9430  cmcm2t 9499  hods 9641  eigpos 9702  nmoprepnf 9734  nmfnrepnf 9747  pjsspos 10038  cvcon3t 10149  mdsymlem8 10274  dmdsymt 10277

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