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 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi1d  346  bibi12d  348  biantr  817  eujust  2599  eujustALT  2600  euf  2604  reu6i  3692  sbc2or  3754  axrep1  5240  axreplem  5241  zfrepclf  5253  axsepg  5259  sepg  5260  zfausclOLD  5262  exnelv  5277  notsep  5336  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  euotd  5498  cnveq0  6198  iota5  6521  eufnfv  7229  isoeq1  7317  isoeq3  7319  isores2  7333  isores3  7335  isotr  7336  isoini2  7339  riota5f  7397  caovordg  7619  caovord  7623  dfoprab4f  8054  seqomlem2  8439  xpf1o  9128  elirrv  9560  aceq0  10103  dfac5  10113  zfac  10445  zfcndrep  10600  zfcndac  10605  ltasr  11086  axpre-ltadd  11153  absmod0  15356  absz  15364  smuval2  16541  prmdvdsexp  16775  isacs2  17710  isacs1i  17714  mreacs  17715  abvfval  20894  abvpropd  20919  isclo2  23226  t0sep  23462  kqt0lem  23874  r0sep  23886  iccpnfcnv  25084  rolle  26130  2sqreultlem  27589  2sqreunnltlem  27592  tgjustr  28721  wlkeq  29961  eigre  32165  fgreu  32994  fcnvgreu  32995  gsumhashmul  33365  xrge0iifcnv  34301  axsepg2  35531  axsepg3  35532  axsepg3ALT  35533  axsepg4  35534  axsepg5  35535  cvmlift2lem13  35785  iota5f  36194  nn0prpwlem  36811  nn0prpw  36812  bj-sepg  37537  bj-inex1gALT  37538  bj-axseprep  37689  bj-axreprepsep  37690  wl-eudf  38205  ismndo2  38503  islaut  40835  ispautN  40851  mrefg2  43418  zindbi  43653  jm2.19lem3  43698  oaordnr  44003  omnord1  44012  oenord1  44023  alephiso2  44264  ntrneiel2  44792  ntrneik4  44807  iotavalb  45120  eusnsn  47740  aiota0def  47810  fargshiftfo  48168  isuspgrimlem  48637  line2x  49511  eufsnlem  49596  thincciso  50208  thinccisod  50209  termcarweu  50283