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  2277  abbi  2291  cleqf  2344  cbvreuvw  2711  vtoclb  2796  vtoclbg  2800  ceqsexg  2867  elabgf  2881  reu6  2928  ru  2963  sbcbig  3011  sbcne12g  3077  sbcnestgf  3110  preq12bg  3775  nalset  4135  undifexmid  4195  exmidsssn  4204  exmidsssnc  4205  exmidundif  4208  opthg  4240  opelopabsb  4262  wetriext  4578  opeliunxp2  4769  resieq  4919  elimasng  4998  cbviota  5185  iota2df  5204  fnbrfvb  5558  fvelimab  5574  fmptco  5684  fsng  5691  fressnfv  5705  funfvima3  5752  isorel  5811  isocnv  5814  isocnv2  5815  isotr  5819  ovg  6015  caovcang  6038  caovordg  6044  caovord3d  6047  caovord  6048  opeliunxp2f  6241  dftpos4  6266  ecopovsym  6633  ecopovsymg  6636  xpf1o  6846  nneneq  6859  supmoti  6994  supsnti  7006  isotilem  7007  isoti  7008  ltanqg  7401  ltmnqg  7402  elinp  7475  prnmaxl  7489  prnminu  7490  ltasrg  7771  axpre-ltadd  7887  zextle  9346  zextlt  9347  xlesubadd  9885  rexfiuz  11000  climshft  11314  dvdsext  11863  ltoddhalfle  11900  halfleoddlt  11901  bezoutlemmo  12009  bezoutlemeu  12010  bezoutlemle  12011  bezoutlemsup  12012  dfgcd3  12013  dvdssq  12034  rpexp  12155  pcdvdsb  12321  isnsg  13067  nsgbi  13069  elnmz  13073  nmzbi  13074  nmznsg  13078  xmeteq0  13898  comet  14038  dedekindeulemuub  14134  dedekindeulemloc  14136  dedekindicclemuub  14143  dedekindicclemloc  14145  logltb  14334  bj-nalset  14686  bj-d0clsepcl  14716  bj-nn0sucALT  14769  ltlenmkv  14857