HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 3bitr4d 548
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
StepHypRef Expression
1 3bitr4d.2 . 2 |- (ph -> (th <-> ps))
2 3bitr4d.1 . . 3 |- (ph -> (ps <-> ch))
3 3bitr4d.3 . . 3 |- (ph -> (ta <-> ch))
42, 3bitr4d 529 . 2 |- (ph -> (ps <-> ta))
51, 4bitrd 526 1 |- (ph -> (th <-> ta))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  sbcom 1253  sbcom2 1329  sbcralt 1980  sbcralgf 1982  sbcel12g 2001  sbceqdig 2002  ordsucelsuc 3063  ordsucsssuc 3064  ordsucun 3072  fvopab3 3762  fvimacnvALT 3794  isotr 3882  isotrALT 3883  oaword 4167  omword 4185  om00el 4191  oeword 4201  brecop 4290  xpdom2 4422  omsucdom 4502  finsucdom 4506  alephord3 4850  ltsopi 4988  ltexpi 5001  ltapi 5002  ltmpi 5003  1idpr 5105  addcanpr 5124  pre-axltadd 5261  subsub23t 5348  axlttri 5475  lemul1t 5788  lediv1t 5806  lt2mul2divt 5822  lediv2t 5839  avglet 5991  nn0subt 6108  zltp1let 6128  qbtwnre 6216  ioonegt 6339  iccnegt 6340  fzaddelt 6432  fzrevt 6443  cj11t 6765  neiint 7660  islp2 7688  nvsubsub23 8222  nmorepnf 8363  shscomt 9198  spansncol 9407  cmcm2t 9476  hods 9618  eigpos 9679  nmoprepnf 9711  nmfnrepnf 9724  pjsspos 10011  cvcon3t 10121  mdsymlem8 10245  dmdsymt 10248
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