Theorem 3bitr4d 550

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

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

This theorem is referenced by:  sbcom 1258  sbcom2 1334  sbcralt 1990  sbcralgf 1992  sbcel12g 2011  sbceqdig 2012  ordsucelsuc 3073  ordsucsssuc 3074  ordsucun 3082  fvopab3 3777  fvimacnvALT 3809  isotr 3897  isotrALT 3898  oaword 4183  omword 4201  om00el 4207  oeword 4217  brecop 4306  xpdom2 4442  omsucdom 4523  finsucdomOLD 4527  alephord3 4878  ltsopi 5016  ltexpi 5029  ltapi 5030  ltmpi 5031  1idpr 5133  addcanpr 5152  pre-axltadd 5289  subsub23t 5376  axlttri 5503  lemul1t 5832  lediv1t 5851  lediv1tOLD 5852  lt2mul2divt 5872  lediv2t 5891  avglet 6044  nn0subt 6161  zltp1let 6181  qbtwnre 6278  ioonegt 6406  iccnegt 6407  fzaddelt 6500  fzrevt 6511  cj11t 6830  neiint 7719  islp2 7747  nvsubsub23 8282  nmorepnf 8431  shscomt 9283  spansncol 9491  cmcm2t 9559  hods 9701  eigpos 9762  nmoprepnf 9794  nmfnrepnf 9807  pjsspos 10100  cvcon3t 10211  mdsymlem8 10337  dmdsymt 10340  hmeobc 10542

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