Theorem 3bitr4g 558

Description: More general version of 3bitr4i 181. Useful for converting definitions in a formula.

Hypotheses

Ref	Expression
3bitr4g.1	|- (ph -> (ps <-> ch))
3bitr4g.2	|- (th <-> ps)
3bitr4g.3	|- (ta <-> ch)

Assertion

Ref	Expression
3bitr4g	|- (ph -> (th <-> ta))

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.1	. . 3 |- (ph -> (ps <-> ch))
2		3bitr4g.2	. . 3 |- (th <-> ps)
3	1, 2	syl5bb 535	. 2 |- (ph -> (th <-> ch))
4		3bitr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6bbr 541	1 |- (ph -> (th <-> ta))

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

This theorem is referenced by:  imbi1d 616  orbi2d 617  orbi1d 618  anbi1d 620  bibi2d 621  bibi1d 622  pm5.32rd 651  3orbi123d 898  3anbi123d 899  drex1 1193  drsb1 1212  cbvexd 1359  sbal2 1397  eubid 1424  mobid 1443  eqeq1 1524  eqeq2 1527  eleq1 1577  eleq2 1578  neeq1 1633  neeq2 1634  neleq1 1688  neleq2 1689  ralbida 1703  rexbida 1704  ralbidv2 1711  rexbidv2 1712  r19.21t 1761  reubidva 1825  raleq1f 1829  rexeq1f 1830  reueq1f 1831  eueq3 1965  dfsbcq 1988  psseq1 2187  psseq2 2188  ssconb 2222  uneq1 2229  ineq1 2262  reuun2 2330  reldisj 2366  undif4 2378  disjssun 2379  intmin4 2626  iindif2 2681  iununi 2686  breq 2694  breq1 2695  breq2 2696  brprc 2734  treq 2760  opeqex 2874  poeq1 2920  soeq1 2932  freq1 2952  weeq1 2964  weeq2 2965  ordeq 2982  limeq 2987  ordunisssuc 3072  rexxfrd 3121  rabxfr 3125  iunpw 3137  tfinds 3212  opthprc 3306  brinxp2 3317  releq 3330  eqrel 3335  eqrelrel 3341  brcnvg 3388  resieq 3463  cores 3602  imadif 3679  fneq1 3688  fneq2 3689  feq1 3727  feq2 3728  feq3 3729  feq23 3730  f1eq1 3767  f1eq2 3768  f1eq3 3769  foeq1 3775  foeq2 3776  foeq3 3777  f1oeq1 3792  f1oeq2 3793  f1oeq3 3794  dffo3 3933  dff13 3988  cbvfo 3999  cbvexfo 4000  isoeq1 4001  isoeq2 4002  isoeq3 4003  isoeq4 4004  isoeq5 4005  isomin 4013  isowe 4017  ereq 4407  erthi 4421  erthdmr 4424  0sdomg 4611  nnsdomo 4668  enfi 4680  isfinite2 4692  brdom7disj 4950  brdom6disj 4951  cardsdom 4986  aleph11 5029  alephiso 5042  ltapq 5230  ltmpq 5231  genpass 5266  distrlem1pr 5281  1idpr 5287  ltasr 5363  ltsor 5415  ltxr 5649  muln0b 5849  le2msqi 6027  msq11i 6028  rpneg 6211  infm3 6222  infmsup 6236  supxrre 6251  dfuzi 6373  icounlem 6539  nn0ennn 7709  znnen 7714  eltopsp 7816  istps2 7819  clsval2 7895  ocin 9445  pjtheu 9512  chpsscon3 9702  pjimai 10384  elat2 10548  mdsymi 10620  prj1 10809  isass 10890  hartoglem 11435  dfcon2 11501  comppfsc 11578  fbunfip 11631  difin2 11791  lmclim2 11915

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 145  df-an 223

Copyright terms: Public domain