Theorem bibi2d 345

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

Ref	Expression
imbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bibi2d	⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 274	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 340	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 306	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 275	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  bibi12d  348  biantr  818  eujust  2602  eujustALT  2603  euf  2607  reu6i  3694  sbc2or  3756  axrep1  5244  axreplem  5245  zfrepclf  5257  axsepg  5263  sepg  5264  zfausclOLD  5266  exnelv  5281  notsep  5339  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  euotd  5501  cnveq0  6201  iota5  6526  eufnfv  7234  isoeq1  7326  isoeq3  7328  isores2  7342  isores3  7344  isotr  7345  isoini2  7348  riota5f  7408  caovordg  7630  caovord  7634  dfoprab4f  8062  seqomlem2  8447  xpf1o  9137  elirrv  9569  aceq0  10121  dfac5  10131  zfac  10462  zfcndrep  10617  zfcndac  10622  ltasr  11103  axpre-ltadd  11170  absmod0  15380  absz  15388  smuval2  16565  prmdvdsexp  16799  isacs2  17734  isacs1i  17738  mreacs  17739  abvfval  20950  abvpropd  20975  isclo2  23282  t0sep  23518  kqt0lem  23930  r0sep  23942  iccpnfcnv  25140  rolle  26186  2sqreultlem  27648  2sqreunnltlem  27651  tgjustr  28780  wlkeq  30020  eigre  32224  fgreu  33053  fcnvgreu  33054  gsumhashmul  33418  xrge0iifcnv  34354  axsepg2  35577  axsepg3  35578  axsepg3ALT  35579  axsepg4  35580  axsepg5  35581  cvmlift2lem13  35828  iota5f  36237  nn0prpwlem  36874  nn0prpw  36875  bj-sepg  37600  bj-inex1gALT  37601  bj-axseprep  37752  bj-axreprepsep  37753  wl-eudf  38268  ismndo2  38566  islaut  40898  ispautN  40914  mrefg2  43479  zindbi  43714  jm2.19lem3  43759  oaordnr  44064  omnord1  44073  oenord1  44084  alephiso2  44325  ntrneiel2  44853  ntrneik4  44868  iotavalb  45181  eusnsn  47804  aiota0def  47874  fargshiftfo  48232  isuspgrimlem  48701  line2x  49575  eufsnlem  49660  thincciso  50272  thinccisod  50273  termcarweu  50347