Theorem bibi2d 343

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bibi1d  344  bibi12d  346  biantr  803  eujust  2571  eujustALT  2572  euf  2576  reu6i  3663  sbc2or  3725  axrep1  5210  axreplem  5211  zfrepclf  5218  axsepg  5224  zfauscl  5225  notzfaus  5285  copsexgw  5404  copsexg  5405  euotd  5427  cnveq0  6100  iotaval  6407  iota5  6416  eufnfv  7105  isoeq1  7188  isoeq3  7190  isores2  7204  isores3  7206  isotr  7207  isoini2  7210  riota5f  7261  caovordg  7479  caovord  7483  dfoprab4f  7896  seqomlem2  8282  xpf1o  8926  aceq0  9874  dfac5  9884  zfac  10216  zfcndrep  10370  zfcndac  10375  ltasr  10856  axpre-ltadd  10923  absmod0  15015  absz  15023  smuval2  16189  prmdvdsexp  16420  isacs2  17362  isacs1i  17366  mreacs  17367  abvfval  20078  abvpropd  20102  isclo2  22239  t0sep  22475  kqt0lem  22887  r0sep  22899  iccpnfcnv  24107  rolle  25154  2sqreultlem  26595  2sqreunnltlem  26598  tgjustr  26835  wlkeq  28001  eigre  30197  fgreu  31009  fcnvgreu  31010  gsumhashmul  31316  xrge0iifcnv  31883  cvmlift2lem13  33277  iota5f  33669  nn0prpwlem  34511  nn0prpw  34512  bj-zfauscl  35112  wl-eudf  35727  ismndo2  36032  islaut  38097  ispautN  38113  mrefg2  40529  zindbi  40768  jm2.19lem3  40813  alephiso2  41165  ntrneiel2  41696  ntrneik4  41711  iotavalb  42048  eusnsn  44520  aiota0def  44588  fargshiftfo  44894  line2x  46100  eufsnlem  46168  thincciso  46330