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  2306  abbi  2320  cleqf  2374  cbvreuvw  2745  vtoclb  2831  vtoclbg  2835  ceqsexg  2902  elabgf  2916  reu6  2963  ru  2998  sbcbig  3046  sbcne12g  3112  sbcnestgf  3146  preq12bg  3816  nalset  4178  undifexmid  4241  exmidsssn  4250  exmidsssnc  4251  exmidundif  4254  opthg  4286  opelopabsb  4310  wetriext  4629  opeliunxp2  4822  resieq  4974  elimasng  5055  cbviota  5242  iota2df  5262  fnbrfvb  5626  fvelimab  5642  fmptco  5753  fsng  5760  fressnfv  5778  funfvima3  5825  isorel  5884  isocnv  5887  isocnv2  5888  isotr  5892  ovg  6092  caovcang  6115  caovordg  6121  caovord3d  6124  caovord  6125  uchoice  6230  opeliunxp2f  6331  dftpos4  6356  ecopovsym  6725  ecopovsymg  6728  xpf1o  6948  nneneq  6961  supmoti  7102  supsnti  7114  isotilem  7115  isoti  7116  ltanqg  7520  ltmnqg  7521  elinp  7594  prnmaxl  7608  prnminu  7609  ltasrg  7890  axpre-ltadd  8006  zextle  9471  zextlt  9472  xlesubadd  10012  rexfiuz  11344  climshft  11659  dvdsext  12210  ltoddhalfle  12248  halfleoddlt  12249  bezoutlemmo  12371  bezoutlemeu  12372  bezoutlemle  12373  bezoutlemsup  12374  dfgcd3  12375  dvdssq  12396  rpexp  12519  pcdvdsb  12687  isnsg  13582  nsgbi  13584  elnmz  13588  nmzbi  13589  nmznsg  13593  islidlm  14285  xmeteq0  14875  comet  15015  dedekindeulemuub  15133  dedekindeulemloc  15135  dedekindicclemuub  15142  dedekindicclemloc  15144  logltb  15390  bj-nalset  15905  bj-d0clsepcl  15935  bj-nn0sucALT  15988  ltlenmkv  16083