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  610  cleqh  2329  abbi  2343  cleqf  2397  cbvreuvw  2771  vtoclb  2859  vtoclbg  2863  ceqsexg  2932  elabgf  2946  reu6  2993  ru  3028  sbcbig  3076  sbcne12g  3143  sbcnestgf  3177  preq12bg  3854  nalset  4217  undifexmid  4281  exmidsssn  4290  exmidsssnc  4291  exmidundif  4294  opthg  4328  opelopabsb  4352  wetriext  4673  opeliunxp2  4868  resieq  5021  elimasng  5102  cbviota  5289  iota2df  5310  fnbrfvb  5680  fvelimab  5698  fmptco  5809  fsng  5816  fressnfv  5836  funfvima3  5883  isorel  5944  isocnv  5947  isocnv2  5948  isotr  5952  ovg  6156  caovcang  6179  caovordg  6185  caovord3d  6188  caovord  6189  uchoice  6295  opeliunxp2f  6399  dftpos4  6424  ecopovsym  6795  ecopovsymg  6798  xpf1o  7025  nneneq  7038  supmoti  7186  supsnti  7198  isotilem  7199  isoti  7200  ltanqg  7613  ltmnqg  7614  elinp  7687  prnmaxl  7701  prnminu  7702  ltasrg  7983  axpre-ltadd  8099  zextle  9564  zextlt  9565  xlesubadd  10111  rexfiuz  11543  climshft  11858  dvdsext  12409  ltoddhalfle  12447  halfleoddlt  12448  bezoutlemmo  12570  bezoutlemeu  12571  bezoutlemle  12572  bezoutlemsup  12573  dfgcd3  12574  dvdssq  12595  rpexp  12718  pcdvdsb  12886  isnsg  13782  nsgbi  13784  elnmz  13788  nmzbi  13789  nmznsg  13793  islidlm  14486  xmeteq0  15076  comet  15216  dedekindeulemuub  15334  dedekindeulemloc  15336  dedekindicclemuub  15343  dedekindicclemloc  15345  logltb  15591  bj-nalset  16440  bj-d0clsepcl  16470  bj-nn0sucALT  16523  ltlenmkv  16624