Theorem 3bitr4g 557

Description: More general version of 3bitr4 183. Useful for converting definitions in a formula.

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2		3bitr4g.2	. . 3 ⊢ (θ ↔ ψ)
3	1, 2	syl5bb 534	. 2 ⊢ (φ → (θ ↔ χ))
4		3bitr4g.3	. 2 ⊢ (τ ↔ χ)
5	3, 4	syl6bbr 540	1 ⊢ (φ → (θ ↔ τ))

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  imbi1d 615  orbi2d 616  orbi1d 617  anbi1d 619  bibi2d 620  bibi1d 621  pm5.32rd 650  3orbi123d 894  3anbi123d 895  drex1 1158  drsb1 1177  cbvexd 1323  sbal2 1360  eubid 1387  mobid 1406  eqeq1 1484  eqeq2 1487  eleq1 1537  eleq2 1538  neeq1 1593  neeq2 1594  neleq1 1645  neleq2 1646  ralbida 1660  rexbida 1661  ralbidv2 1668  rexbidv2 1669  r19.21t 1718  reubidva 1782  raleq1f 1786  rexeq1f 1787  reueq1f 1788  eueq3 1922  dfsbcq 1946  psseq1 2138  psseq2 2139  ssconb 2173  uneq1 2180  ineq1 2213  reuun2 2281  reldisj 2317  undif4 2329  disjssun 2330  intmin4 2563  iindif2 2616  iununi 2621  breq 2626  breq1 2627  breq2 2628  brprc 2666  treq 2691  opeqex 2804  poeq1 2848  soeq1 2859  rexxfrd 2904  rabxfr 2908  iunpw 2920  freq1 2928  weeq1 2943  weeq2 2944  ordeq 2961  limeq 2966  ordunisssuc 3089  tfinds 3167  opthprc 3227  brinxp2 3237  releq 3249  eqrel 3256  brcnvg 3303  resieq 3382  cores 3505  imadif 3580  fneq1 3588  fneq2 3589  feq1 3626  feq2 3627  feq3 3628  feq23 3629  f1eq1 3666  f1eq2 3667  f1eq3 3668  foeq1 3674  foeq2 3675  foeq3 3676  f1oeq1 3690  f1oeq2 3691  f1oeq3 3692  dffo3 3825  f1fv 3880  cbvfo 3891  cbvexfo 3892  isoeq1 3893  isoeq2 3894  isoeq3 3895  isoeq4 3896  isoeq5 3897  isomin 3905  isowe 3909  2ndconst 4103  dfoprab5 4121  ereq 4273  erthi 4287  erthdmr 4290  0sdomg 4472  nnsdomo 4527  enfi 4543  isfinite2 4557  isfinite2OLD 4558  brdom7disj 4814  brdom6disj 4815  cardsdom 4847  aleph11 4890  alephiso 4903  ltapq 5088  ltmpq 5089  genpass 5124  distrlem1pr 5139  1idpr 5145  ltasr 5221  ltsor 5273  ltxrt 5507  muln0bt 5709  le2msq 5884  msq11 5885  infm3 6056  infmsup 6070  supxrre 6085  dfuz 6204  icounlem 6413  nn0ennn 7498  znnen 7503  eltopsp 7605  istps2 7608  clsval2 7682  ocin 9164  pjtheut 9231  chpsscon3t 9421  pjima 10099  elat2 10262  mdsym 10333

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