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  806  eujust  2569  eujustALT  2570  euf  2574  reu6i  3737  sbc2or  3800  axrep1  5286  axreplem  5287  zfrepclf  5297  axsepg  5303  zfauscl  5304  notzfaus  5369  copsexgw  5501  copsexg  5502  euotd  5523  cnveq0  6219  iotavalOLD  6537  iota5  6546  eufnfv  7249  isoeq1  7337  isoeq3  7339  isores2  7353  isores3  7355  isotr  7356  isoini2  7359  riota5f  7416  caovordg  7640  caovord  7644  dfoprab4f  8080  seqomlem2  8490  xpf1o  9178  aceq0  10156  dfac5  10167  zfac  10498  zfcndrep  10652  zfcndac  10657  ltasr  11138  axpre-ltadd  11205  absmod0  15339  absz  15347  smuval2  16516  prmdvdsexp  16749  isacs2  17698  isacs1i  17702  mreacs  17703  abvfval  20828  abvpropd  20853  isclo2  23112  t0sep  23348  kqt0lem  23760  r0sep  23772  iccpnfcnv  24989  rolle  26043  2sqreultlem  27506  2sqreunnltlem  27509  tgjustr  28497  wlkeq  29667  eigre  31864  fgreu  32689  fcnvgreu  32690  gsumhashmul  33047  xrge0iifcnv  33894  axsepg2  35075  axsepg2ALT  35076  cvmlift2lem13  35300  iota5f  35704  nn0prpwlem  36305  nn0prpw  36306  bj-zfauscl  36907  wl-eudf  37553  ismndo2  37861  islaut  40066  ispautN  40082  mrefg2  42695  zindbi  42935  jm2.19lem3  42980  oaordnr  43286  omnord1  43295  oenord1  43306  alephiso2  43548  ntrneiel2  44076  ntrneik4  44091  iotavalb  44426  eusnsn  46976  aiota0def  47046  fargshiftfo  47367  isuspgrimlem  47812  line2x  48604  eufsnlem  48671  thincciso  48849  thinccisod  48850