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  2570  eujustALT  2571  euf  2575  reu6i  3733  sbc2or  3796  axrep1  5279  axreplem  5280  zfrepclf  5290  axsepg  5296  zfauscl  5297  notzfaus  5362  copsexgw  5494  copsexg  5495  euotd  5517  cnveq0  6216  iotavalOLD  6534  iota5  6543  eufnfv  7250  isoeq1  7338  isoeq3  7340  isores2  7354  isores3  7356  isotr  7357  isoini2  7360  riota5f  7417  caovordg  7641  caovord  7645  dfoprab4f  8082  seqomlem2  8492  xpf1o  9180  aceq0  10159  dfac5  10170  zfac  10501  zfcndrep  10655  zfcndac  10660  ltasr  11141  axpre-ltadd  11208  absmod0  15343  absz  15351  smuval2  16520  prmdvdsexp  16753  isacs2  17697  isacs1i  17701  mreacs  17702  abvfval  20812  abvpropd  20837  isclo2  23097  t0sep  23333  kqt0lem  23745  r0sep  23757  iccpnfcnv  24976  rolle  26029  2sqreultlem  27492  2sqreunnltlem  27495  tgjustr  28483  wlkeq  29653  eigre  31855  fgreu  32683  fcnvgreu  32684  gsumhashmul  33065  xrge0iifcnv  33933  axsepg2  35097  axsepg2ALT  35098  cvmlift2lem13  35321  iota5f  35725  nn0prpwlem  36324  nn0prpw  36325  bj-zfauscl  36926  wl-eudf  37574  ismndo2  37882  islaut  40086  ispautN  40102  mrefg2  42723  zindbi  42963  jm2.19lem3  43008  oaordnr  43314  omnord1  43323  oenord1  43334  alephiso2  43576  ntrneiel2  44104  ntrneik4  44119  iotavalb  44454  eusnsn  47043  aiota0def  47113  fargshiftfo  47434  isuspgrimlem  47879  line2x  48680  eufsnlem  48755  thincciso  49127  thinccisod  49128  termcarweu  49186