Theorem bibi2d 345

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  bibi12d  348  biantr  818  eujust  2597  eujustALT  2598  euf  2602  reu6i  3686  sbc2or  3748  axrep1  5233  axreplem  5234  zfrepclf  5244  axsepg  5250  sepg  5251  zfausclOLD  5253  exnelv  5267  notsep  5325  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  euotd  5486  cnveq0  6189  iota5  6514  eufnfv  7227  isoeq1  7317  isoeq3  7319  isores2  7333  isores3  7335  isotr  7336  isoini2  7339  riota5f  7397  caovordg  7620  caovord  7624  dfoprab4f  8056  seqomlem2  8445  xpf1o  9142  elirrv  9575  aceq0  10178  dfac5  10188  zfac  10519  zfcndrep  10680  zfcndac  10685  ltasr  11166  axpre-ltadd  11233  absmod0  15450  absz  15458  smuval2  16632  prmdvdsexp  16871  isacs2  17807  isacs1i  17811  mreacs  17812  abvfval  21047  abvpropd  21072  isclo2  23386  t0sep  23622  kqt0lem  24035  r0sep  24047  iccpnfcnv  25245  rolle  26290  2sqreultlem  27756  2sqreunnltlem  27759  tgjustr  28918  wlkeq  30196  eigre  32419  fgreu  33247  fcnvgreu  33248  gsumhashmul  33610  xrge0iifcnv  34547  axsepg2  35781  axsepg3  35782  axsepg3ALT  35783  axsepg4  35784  axsepg5  35785  cvmlift2lem13  36049  iota5f  36458  nn0prpwlem  37080  nn0prpw  37081  bj-sepg  37806  bj-inex1gALT  37807  bj-axseprep  37958  bj-axreprepsep  37959  wl-eudf  38472  ismndo2  38776  islaut  41108  ispautN  41124  mrefg2  43671  zindbi  43906  jm2.19lem3  43951  oaordnr  44256  omnord1  44265  oenord1  44276  alephiso2  44517  ntrneiel2  45045  ntrneik4  45060  iotavalb  45373  eusnsn  48040  aiota0def  48110  fargshiftfo  48468  isuspgrimlem  48937  line2x  49810  eufsnlem  49895  thincciso  50505  thinccisod  50506  termcarweu  50580