Theorem 3bitr4g 279

Description: More general version of 3bitr4i 268. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr4g

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

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bibi1d  310  pm5.32rd  621  orbi2d  682  orbi1d  683  3orbi123d  1251  3anbi123d  1252  nanbi1  1295  nanbi2  1296  xorbi12d  1315  hadbi123d  1382  cadbi123d  1383  cad1  1398  had0  1403  nfbidf  1774  drex1  1967  drnf1  1969  drnf2  1970  cbvexd  2009  drsb1  2022  sbal2  2134  eujustALT  2207  eubid  2211  mobid  2238  eqeq1  2359  eqeq2  2362  eleq1  2413  eleq2  2414  nfceqdf  2488  drnfc1  2505  drnfc2  2506  neeq1  2524  neeq2  2525  neleq1  2607  neleq2  2608  ralbida  2628  rexbida  2629  ralbidv2  2636  rexbidv2  2637  r19.21t  2699  r19.23t  2728  ralcom2  2775  reubida  2793  rmobida  2798  raleqf  2803  rexeqf  2804  reueq1f  2805  rmoeq1f  2806  cbvraldva2  2839  cbvrexdva2  2840  dfsbcq  3048  sbcbid  3099  sbcrext  3119  sbcabel  3123  sbnfc2  3196  elin  3219  elun  3220  psseq1  3356  psseq2  3357  ssconb  3399  uneq1  3411  ineq1  3450  difin2  3516  reuun2  3538  reldisj  3594  undif4  3607  disjssun  3608  pssdifcom1  3635  pssdifcom2  3636  sbcss  3660  eltpg  3769  raltpg  3777  rextpg  3778  intmin4  3955  dfiun2g  3999  iindif2  4035  iinin2  4036  iinxprg  4043  ssofeq  4077  xpkeq1  4198  xpkeq2  4199  opkelimagekg  4271  iotaeq  4347  sniota  4369  sfineq1  4526  sfineq2  4527  phialllem1  4616  breq  4641  breq1  4642  breq2  4643  elimasn  5019  dfco2a  5081  imadif  5171  fneq1  5173  fneq2  5174  feq1  5210  feq2  5211  feq3  5212  fcnvres  5243  f1eq1  5253  f1eq2  5254  f1eq3  5255  foeq1  5265  foeq2  5266  foeq3  5267  f1oeq1  5281  f1oeq2  5282  f1oeq3  5283  fun11iun  5305  dmfco  5381  dffo3  5422  funiunfv  5467  dff13  5471  isoeq1  5482  isoeq2  5483  isoeq3  5484  isoeq4  5485  isoeq5  5486  isomin  5496  mpt2eq123  5661  clos1basesucg  5884  erdmrn  5965  ereldm  5971  ce0nnul  6177  nmembers1lem3  6270  epelcres  6328