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  2599  eujustALT  2600  euf  2604  reu6i  3689  sbc2or  3751  axrep1  5237  axreplem  5238  zfrepclf  5248  axsepg  5254  sepg  5255  zfausclOLD  5257  exnelv  5271  notsep  5330  copsexgw  5465  copsexgwOLD  5466  copsexg  5467  cotsexgw  5468  euotd  5491  iota5  6543  eufnfv  7261  isoeq1  7351  isoeq3  7353  isores2  7367  isores3  7369  isotr  7370  isoini2  7373  riota5f  7431  caovordg  7655  caovord  7659  dfoprab4f  8095  seqomlem2  8492  xpf1o  9189  elirrv  9621  aceq0  10227  dfac5  10237  zfac  10568  zfcndrep  10729  zfcndac  10734  ltasr  11215  axpre-ltadd  11282  absmod0  15502  absz  15510  smuval2  16684  prmdvdsexp  16923  isacs2  17859  isacs1i  17863  mreacs  17864  abvfval  21100  abvpropd  21125  isclo2  23439  t0sep  23675  kqt0lem  24088  r0sep  24100  iccpnfcnv  25298  rolle  26343  2sqreultlem  27807  2sqreunnltlem  27810  tgjustr  28969  wlkeq  30247  eigre  32470  fgreu  33340  fcnvgreu  33341  gsumhashmul  33704  xrge0iifcnv  34648  axsepg2  35921  axsepg3  35922  axsepg3ALT  35923  axsepg4  35924  axsepg5  35925  srepdflem2  36099  srepdf  36100  cvmlift2lem13  36260  iota5f  36680  nn0prpwlem  37301  nn0prpw  37302  bj-sepg  38027  bj-inex1gALT  38028  bj-axseprep  38194  bj-axreprepsep  38195  wl-eudf  38709  ismndo2  39011  islaut  41343  ispautN  41359  mrefg2  43922  zindbi  44157  jm2.19lem3  44202  oaordnr  44501  omnord1  44510  oenord1  44521  alephiso2  44762  ntrneiel2  45289  ntrneik4  45304  iotavalb  45616  eusnsn  48311  aiota0def  48381  fargshiftfo  48739  isuspgrimlem  49208  line2x  50081  eufsnlem  50167  thincciso  50803  thinccisod  50804  termcarweu  50878