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  2858  vtoclbg  2862  ceqsexg  2931  elabgf  2945  reu6  2992  ru  3027  sbcbig  3075  sbcne12g  3142  sbcnestgf  3176  preq12bg  3851  nalset  4214  undifexmid  4278  exmidsssn  4287  exmidsssnc  4288  exmidundif  4291  opthg  4325  opelopabsb  4349  wetriext  4670  opeliunxp2  4865  resieq  5018  elimasng  5099  cbviota  5286  iota2df  5307  fnbrfvb  5677  fvelimab  5695  fmptco  5806  fsng  5813  fressnfv  5833  funfvima3  5880  isorel  5941  isocnv  5944  isocnv2  5945  isotr  5949  ovg  6153  caovcang  6176  caovordg  6182  caovord3d  6185  caovord  6186  uchoice  6292  opeliunxp2f  6395  dftpos4  6420  ecopovsym  6791  ecopovsymg  6794  xpf1o  7018  nneneq  7031  supmoti  7176  supsnti  7188  isotilem  7189  isoti  7190  ltanqg  7603  ltmnqg  7604  elinp  7677  prnmaxl  7691  prnminu  7692  ltasrg  7973  axpre-ltadd  8089  zextle  9554  zextlt  9555  xlesubadd  10096  rexfiuz  11521  climshft  11836  dvdsext  12387  ltoddhalfle  12425  halfleoddlt  12426  bezoutlemmo  12548  bezoutlemeu  12549  bezoutlemle  12550  bezoutlemsup  12551  dfgcd3  12552  dvdssq  12573  rpexp  12696  pcdvdsb  12864  isnsg  13760  nsgbi  13762  elnmz  13766  nmzbi  13767  nmznsg  13771  islidlm  14464  xmeteq0  15054  comet  15194  dedekindeulemuub  15312  dedekindeulemloc  15314  dedekindicclemuub  15321  dedekindicclemloc  15323  logltb  15569  bj-nalset  16367  bj-d0clsepcl  16397  bj-nn0sucALT  16450  ltlenmkv  16552