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  608  cleqh  2296  abbi  2310  cleqf  2364  cbvreuvw  2735  vtoclb  2821  vtoclbg  2825  ceqsexg  2892  elabgf  2906  reu6  2953  ru  2988  sbcbig  3036  sbcne12g  3102  sbcnestgf  3136  preq12bg  3803  nalset  4163  undifexmid  4226  exmidsssn  4235  exmidsssnc  4236  exmidundif  4239  opthg  4271  opelopabsb  4294  wetriext  4613  opeliunxp2  4806  resieq  4956  elimasng  5037  cbviota  5224  iota2df  5244  fnbrfvb  5601  fvelimab  5617  fmptco  5728  fsng  5735  fressnfv  5749  funfvima3  5796  isorel  5855  isocnv  5858  isocnv2  5859  isotr  5863  ovg  6062  caovcang  6085  caovordg  6091  caovord3d  6094  caovord  6095  uchoice  6195  opeliunxp2f  6296  dftpos4  6321  ecopovsym  6690  ecopovsymg  6693  xpf1o  6905  nneneq  6918  supmoti  7059  supsnti  7071  isotilem  7072  isoti  7073  ltanqg  7467  ltmnqg  7468  elinp  7541  prnmaxl  7555  prnminu  7556  ltasrg  7837  axpre-ltadd  7953  zextle  9417  zextlt  9418  xlesubadd  9958  rexfiuz  11154  climshft  11469  dvdsext  12020  ltoddhalfle  12058  halfleoddlt  12059  bezoutlemmo  12173  bezoutlemeu  12174  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  dvdssq  12198  rpexp  12321  pcdvdsb  12489  isnsg  13332  nsgbi  13334  elnmz  13338  nmzbi  13339  nmznsg  13343  islidlm  14035  xmeteq0  14595  comet  14735  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindicclemuub  14862  dedekindicclemloc  14864  logltb  15110  bj-nalset  15541  bj-d0clsepcl  15571  bj-nn0sucALT  15624  ltlenmkv  15714