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  2293  abbi  2307  cleqf  2361  cbvreuvw  2732  vtoclb  2817  vtoclbg  2821  ceqsexg  2888  elabgf  2902  reu6  2949  ru  2984  sbcbig  3032  sbcne12g  3098  sbcnestgf  3132  preq12bg  3799  nalset  4159  undifexmid  4222  exmidsssn  4231  exmidsssnc  4232  exmidundif  4235  opthg  4267  opelopabsb  4290  wetriext  4609  opeliunxp2  4802  resieq  4952  elimasng  5033  cbviota  5220  iota2df  5240  fnbrfvb  5597  fvelimab  5613  fmptco  5724  fsng  5731  fressnfv  5745  funfvima3  5792  isorel  5851  isocnv  5854  isocnv2  5855  isotr  5859  ovg  6057  caovcang  6080  caovordg  6086  caovord3d  6089  caovord  6090  uchoice  6190  opeliunxp2f  6291  dftpos4  6316  ecopovsym  6685  ecopovsymg  6688  xpf1o  6900  nneneq  6913  supmoti  7052  supsnti  7064  isotilem  7065  isoti  7066  ltanqg  7460  ltmnqg  7461  elinp  7534  prnmaxl  7548  prnminu  7549  ltasrg  7830  axpre-ltadd  7946  zextle  9408  zextlt  9409  xlesubadd  9949  rexfiuz  11133  climshft  11447  dvdsext  11997  ltoddhalfle  12034  halfleoddlt  12035  bezoutlemmo  12143  bezoutlemeu  12144  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dvdssq  12168  rpexp  12291  pcdvdsb  12458  isnsg  13272  nsgbi  13274  elnmz  13278  nmzbi  13279  nmznsg  13283  islidlm  13975  xmeteq0  14527  comet  14667  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindicclemuub  14780  dedekindicclemloc  14782  logltb  15009  bj-nalset  15387  bj-d0clsepcl  15417  bj-nn0sucALT  15470  ltlenmkv  15560