Theorem 3bitr4d 552

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

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (φ → (ψ ↔ χ))
3bitr4d.2	⊢ (φ → (θ ↔ ψ))
3bitr4d.3	⊢ (φ → (τ ↔ χ))

Assertion

Ref	Expression
3bitr4d	⊢ (φ → (θ ↔ τ))

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (φ → (θ ↔ ψ))
2		3bitr4d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
3		3bitr4d.3	. . 3 ⊢ (φ → (τ ↔ χ))
4	2, 3	bitr4d 533	. 2 ⊢ (φ → (ψ ↔ τ))
5	1, 4	bitrd 530	1 ⊢ (φ → (θ ↔ τ))

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  sbcom 1260  sbcom2 1336  sbcralt 1993  sbcralgf 1995  sbcel12g 2014  sbceqdig 2015  ordsucelsuc 3079  ordsucsssuc 3080  ordsucun 3088  fvopab3 3783  fvimacnvALT 3815  isotr 3903  isotrALT 3904  oaword 4189  omword 4207  om00el 4213  oeword 4223  brecop 4312  xpdom2 4448  omsucdom 4528  finsucdom 4532  finsucdomOLD 4533  alephord3 4889  ltsopi 5028  ltexpi 5041  ltapi 5042  ltmpi 5043  1idpr 5145  addcanpr 5164  pre-axltadd 5301  subsub23t 5388  axlttri 5515  lemul1t 5834  lediv1t 5853  lediv1tOLD 5854  lt2mul2divt 5874  lediv2t 5893  avglet 6046  nn0subt 6163  zltp1let 6183  qbtwnre 6279  ioonegt 6407  iccnegt 6408  fzaddelt 6501  fzrevt 6512  cj11t 6830  neiint 7716  islp2 7744  nvsubsub23 8278  nmorepnf 8427  shscomt 9278  spansncol 9486  cmcm2t 9554  hods 9696  eigpos 9757  nmoprepnf 9789  nmfnrepnf 9802  pjsspos 10095  cvcon3t 10206  mdsymlem8 10332  dmdsymt 10335  hmeobc 10528

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