Theorem bibi2d 343

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 272	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 338	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 271	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 271	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 304	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 273	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bibi1d  344  bibi12d  346  biantr  811  eujust  2575  eujustALT  2576  euf  2580  reu6i  3676  sbc2or  3739  axrep1  5207  axreplem  5208  zfrepclf  5220  axsepg  5226  zfauscl  5227  exnelv  5242  notzfaus  5299  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  euotd  5461  cnveq0  6155  iota5  6475  eufnfv  7180  isoeq1  7268  isoeq3  7270  isores2  7284  isores3  7286  isotr  7287  isoini2  7290  riota5f  7348  caovordg  7570  caovord  7574  dfoprab4f  8005  seqomlem2  8387  xpf1o  9074  elirrv  9509  aceq0  10038  dfac5  10049  zfac  10380  zfcndrep  10535  zfcndac  10540  ltasr  11021  axpre-ltadd  11088  absmod0  15263  absz  15271  smuval2  16449  prmdvdsexp  16683  isacs2  17617  isacs1i  17621  mreacs  17622  abvfval  20789  abvpropd  20814  isclo2  23078  t0sep  23314  kqt0lem  23726  r0sep  23738  iccpnfcnv  24936  rolle  25982  2sqreultlem  27435  2sqreunnltlem  27438  tgjustr  28567  wlkeq  29727  eigre  31931  fgreu  32770  fcnvgreu  32771  gsumhashmul  33155  xrge0iifcnv  34124  axsepg2  35328  axsepg3  35329  axsepg3ALT  35330  axsepg4  35331  axsepg5  35332  cvmlift2lem13  35550  iota5f  35959  nn0prpwlem  36557  nn0prpw  36558  bj-zfauscl  37284  bj-axseprep  37434  bj-axreprepsep  37435  wl-eudf  37950  ismndo2  38248  islaut  40582  ispautN  40598  mrefg2  43163  zindbi  43398  jm2.19lem3  43443  oaordnr  43748  omnord1  43757  oenord1  43768  alephiso2  44009  ntrneiel2  44537  ntrneik4  44552  iotavalb  44881  eusnsn  47496  aiota0def  47566  fargshiftfo  47924  isuspgrimlem  48393  line2x  49252  eufsnlem  49338  thincciso  49950  thinccisod  49951  termcarweu  50025