Theorem bibi12d 235

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 233	. 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	bibi2d 232	. 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32  453  bi2bian9  612  cleqh  2330  abbi  2344  cleqf  2398  cbvreuvw  2772  vtoclb  2860  vtoclbg  2864  ceqsexg  2933  elabgf  2947  reu6  2994  ru  3029  sbcbig  3077  sbcne12g  3144  sbcnestgf  3178  preq12bg  3857  nalset  4220  undifexmid  4285  exmidsssn  4294  exmidsssnc  4295  exmidundif  4298  opthg  4332  opelopabsb  4356  wetriext  4677  opeliunxp2  4872  resieq  5025  elimasng  5106  cbviota  5293  iota2df  5314  fnbrfvb  5687  fvelimab  5705  fmptco  5816  fsng  5823  fressnfv  5844  funfvima3  5893  isorel  5954  isocnv  5957  isocnv2  5958  isotr  5962  ovg  6166  caovcang  6189  caovordg  6195  caovord3d  6198  caovord  6199  uchoice  6305  opeliunxp2f  6409  dftpos4  6434  ecopovsym  6805  ecopovsymg  6808  xpf1o  7035  nneneq  7048  supmoti  7197  supsnti  7209  isotilem  7210  isoti  7211  ltanqg  7625  ltmnqg  7626  elinp  7699  prnmaxl  7713  prnminu  7714  ltasrg  7995  axpre-ltadd  8111  zextle  9576  zextlt  9577  xlesubadd  10123  rexfiuz  11572  climshft  11887  dvdsext  12439  ltoddhalfle  12477  halfleoddlt  12478  bezoutlemmo  12600  bezoutlemeu  12601  bezoutlemle  12602  bezoutlemsup  12603  dfgcd3  12604  dvdssq  12625  rpexp  12748  pcdvdsb  12916  isnsg  13812  nsgbi  13814  elnmz  13818  nmzbi  13819  nmznsg  13823  islidlm  14517  xmeteq0  15112  comet  15252  dedekindeulemuub  15370  dedekindeulemloc  15372  dedekindicclemuub  15379  dedekindicclemloc  15381  logltb  15627  eupth2lem3lem6fi  16351  bj-nalset  16550  bj-d0clsepcl  16580  bj-nn0sucALT  16633  ltlenmkv  16742