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  2309  abbi  2323  cleqf  2377  cbvreuvw  2751  vtoclb  2838  vtoclbg  2842  ceqsexg  2911  elabgf  2925  reu6  2972  ru  3007  sbcbig  3055  sbcne12g  3122  sbcnestgf  3156  preq12bg  3830  nalset  4193  undifexmid  4256  exmidsssn  4265  exmidsssnc  4266  exmidundif  4269  opthg  4303  opelopabsb  4327  wetriext  4646  opeliunxp2  4839  resieq  4991  elimasng  5072  cbviota  5259  iota2df  5280  fnbrfvb  5646  fvelimab  5663  fmptco  5774  fsng  5781  fressnfv  5799  funfvima3  5846  isorel  5905  isocnv  5908  isocnv2  5909  isotr  5913  ovg  6115  caovcang  6138  caovordg  6144  caovord3d  6147  caovord  6148  uchoice  6253  opeliunxp2f  6354  dftpos4  6379  ecopovsym  6748  ecopovsymg  6751  xpf1o  6973  nneneq  6986  supmoti  7128  supsnti  7140  isotilem  7141  isoti  7142  ltanqg  7555  ltmnqg  7556  elinp  7629  prnmaxl  7643  prnminu  7644  ltasrg  7925  axpre-ltadd  8041  zextle  9506  zextlt  9507  xlesubadd  10047  rexfiuz  11466  climshft  11781  dvdsext  12332  ltoddhalfle  12370  halfleoddlt  12371  bezoutlemmo  12493  bezoutlemeu  12494  bezoutlemle  12495  bezoutlemsup  12496  dfgcd3  12497  dvdssq  12518  rpexp  12641  pcdvdsb  12809  isnsg  13705  nsgbi  13707  elnmz  13711  nmzbi  13712  nmznsg  13716  islidlm  14408  xmeteq0  14998  comet  15138  dedekindeulemuub  15256  dedekindeulemloc  15258  dedekindicclemuub  15265  dedekindicclemloc  15267  logltb  15513  bj-nalset  16168  bj-d0clsepcl  16198  bj-nn0sucALT  16251  ltlenmkv  16349