Theorem bibi2d 344

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 273	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 339	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 272	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 272	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 305	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 274	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi1d  345  bibi12d  347  biantr  815  eujust  2597  eujustALT  2598  euf  2602  reu6i  3690  sbc2or  3753  axrep1  5227  axreplem  5228  zfrepclf  5240  axsepg  5246  zfauscl  5247  exnelv  5262  notzfaus  5319  copsexgw  5457  copsexgwOLD  5458  copsexg  5459  euotd  5481  cnveq0  6180  iota5  6500  eufnfv  7209  isoeq1  7297  isoeq3  7299  isores2  7313  isores3  7315  isotr  7316  isoini2  7319  riota5f  7377  caovordg  7599  caovord  7603  dfoprab4f  8033  seqomlem2  8417  xpf1o  9107  elirrv  9542  aceq0  10071  dfac5  10082  zfac  10414  zfcndrep  10569  zfcndac  10574  ltasr  11055  axpre-ltadd  11122  absmod0  15313  absz  15321  smuval2  16499  prmdvdsexp  16733  isacs2  17668  isacs1i  17672  mreacs  17673  abvfval  20839  abvpropd  20864  isclo2  23128  t0sep  23364  kqt0lem  23776  r0sep  23788  iccpnfcnv  24986  rolle  26032  2sqreultlem  27488  2sqreunnltlem  27491  tgjustr  28620  wlkeq  29780  eigre  31984  fgreu  32823  fcnvgreu  32824  gsumhashmul  33208  xrge0iifcnv  34191  axsepg2  35400  axsepg3  35401  axsepg3ALT  35402  axsepg4  35403  axsepg5  35404  cvmlift2lem13  35629  iota5f  36038  nn0prpwlem  36646  nn0prpw  36647  bj-zfauscl  37373  bj-axseprep  37523  bj-axreprepsep  37524  wl-eudf  38039  ismndo2  38337  islaut  40671  ispautN  40687  mrefg2  43252  zindbi  43487  jm2.19lem3  43532  oaordnr  43837  omnord1  43846  oenord1  43857  alephiso2  44098  ntrneiel2  44626  ntrneik4  44641  iotavalb  44970  eusnsn  47584  aiota0def  47654  fargshiftfo  48012  isuspgrimlem  48481  line2x  49340  eufsnlem  49426  thincciso  50038  thinccisod  50039  termcarweu  50113