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  2596  eujustALT  2597  euf  2601  reu6i  3685  sbc2or  3747  axrep1  5232  axreplem  5233  zfrepclf  5243  axsepg  5249  sepg  5250  zfausclOLD  5252  exnelv  5266  notsep  5324  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  euotd  5485  iota5  6521  eufnfv  7235  isoeq1  7325  isoeq3  7327  isores2  7341  isores3  7343  isotr  7344  isoini2  7347  riota5f  7405  caovordg  7628  caovord  7632  dfoprab4f  8067  seqomlem2  8464  xpf1o  9161  elirrv  9594  aceq0  10200  dfac5  10210  zfac  10541  zfcndrep  10702  zfcndac  10707  ltasr  11188  axpre-ltadd  11255  absmod0  15475  absz  15483  smuval2  16657  prmdvdsexp  16896  isacs2  17832  isacs1i  17836  mreacs  17837  abvfval  21072  abvpropd  21097  isclo2  23411  t0sep  23647  kqt0lem  24060  r0sep  24072  iccpnfcnv  25270  rolle  26315  2sqreultlem  27779  2sqreunnltlem  27782  tgjustr  28941  wlkeq  30219  eigre  32442  fgreu  33312  fcnvgreu  33313  gsumhashmul  33674  xrge0iifcnv  34611  axsepg2  35864  axsepg3  35865  axsepg3ALT  35866  axsepg4  35867  axsepg5  35868  srepdflem2  36005  srepdf  36006  cvmlift2lem13  36166  iota5f  36581  nn0prpwlem  37202  nn0prpw  37203  bj-sepg  37928  bj-inex1gALT  37929  bj-axseprep  38082  bj-axreprepsep  38083  wl-eudf  38597  ismndo2  38901  islaut  41233  ispautN  41249  mrefg2  43811  zindbi  44046  jm2.19lem3  44091  oaordnr  44391  omnord1  44400  oenord1  44411  alephiso2  44652  ntrneiel2  45179  ntrneik4  45194  iotavalb  45507  eusnsn  48189  aiota0def  48259  fargshiftfo  48617  isuspgrimlem  49086  line2x  49959  eufsnlem  50045  thincciso  50681  thinccisod  50682  termcarweu  50756