Theorem bibi2d 342

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 271	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 337	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 270	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 270	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 303	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 272	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bibi1d  343  bibi12d  345  biantr  805  eujust  2565  eujustALT  2566  euf  2570  reu6i  3702  sbc2or  3765  axrep1  5238  axreplem  5239  zfrepclf  5249  axsepg  5255  zfauscl  5256  notzfaus  5321  copsexgw  5453  copsexg  5454  euotd  5476  cnveq0  6173  iotavalOLD  6488  iota5  6497  eufnfv  7206  isoeq1  7295  isoeq3  7297  isores2  7311  isores3  7313  isotr  7314  isoini2  7317  riota5f  7375  caovordg  7599  caovord  7603  dfoprab4f  8038  seqomlem2  8422  xpf1o  9109  aceq0  10078  dfac5  10089  zfac  10420  zfcndrep  10574  zfcndac  10579  ltasr  11060  axpre-ltadd  11127  absmod0  15276  absz  15284  smuval2  16459  prmdvdsexp  16692  isacs2  17621  isacs1i  17625  mreacs  17626  abvfval  20726  abvpropd  20751  isclo2  22982  t0sep  23218  kqt0lem  23630  r0sep  23642  iccpnfcnv  24849  rolle  25901  2sqreultlem  27365  2sqreunnltlem  27368  tgjustr  28408  wlkeq  29569  eigre  31771  fgreu  32603  fcnvgreu  32604  gsumhashmul  33008  xrge0iifcnv  33930  axsepg2  35079  axsepg2ALT  35080  cvmlift2lem13  35309  iota5f  35718  nn0prpwlem  36317  nn0prpw  36318  bj-zfauscl  36919  wl-eudf  37567  ismndo2  37875  islaut  40084  ispautN  40100  mrefg2  42702  zindbi  42942  jm2.19lem3  42987  oaordnr  43292  omnord1  43301  oenord1  43312  alephiso2  43554  ntrneiel2  44082  ntrneik4  44097  iotavalb  44426  eusnsn  47031  aiota0def  47101  fargshiftfo  47447  isuspgrimlem  47899  line2x  48747  eufsnlem  48833  thincciso  49446  thinccisod  49447  termcarweu  49521