Theorem bibi12d 312

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
bibi12d	⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ τ)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	bibi1d 310	. 2 ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ θ)))
3		imbi12d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	bibi2d 309	. 2 ⊢ (φ → ((χ ↔ θ) ↔ (χ ↔ τ)))
5	2, 4	bitrd 244	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:  bi2bian9  845  xorbi12d  1315  cleqh  2450  abbi  2463  cleqf  2513  vtoclb  2912  vtoclbg  2915  ceqsexg  2970  elabgf  2983  reu6  3025  ru  3045  sbcbig  3092  sbcnestgf  3183  unineq  3505  preq12bg  4128  eqpw1  4162  pw111  4170  eqrelk  4212  opkelimagekg  4271  sikexlem  4295  insklem  4304  eqpw1uni  4330  cbviota  4344  iota2df  4365  opelopabsb  4697  br1stg  4730  opeliunxp2  4822  fvelimab  5370  eqfnfv  5392  fsng  5433  fressnfv  5439  isorel  5489  isocnv  5491  isotr  5495  caovord  5629  trtxp  5781  oqelins4  5794  txpcofun  5803  qrpprod  5836  fnfullfunlem1  5856  clos1basesucg  5884  extd  5923  xpassen  6057  enpw1  6062  dflec3  6221  lenc  6223  tc11  6228