Theorem bibi2d 342

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bibi1d  343  bibi12d  345  biantr  806  eujust  2572  eujustALT  2573  euf  2577  reu6i  3675  sbc2or  3738  axrep1  5213  axreplem  5214  zfrepclf  5226  axsepg  5232  zfauscl  5233  exnelv  5248  notzfaus  5300  copsexgw  5438  copsexg  5439  euotd  5461  cnveq0  6155  iota5  6475  eufnfv  7177  isoeq1  7265  isoeq3  7267  isores2  7281  isores3  7283  isotr  7284  isoini2  7287  riota5f  7345  caovordg  7567  caovord  7571  dfoprab4f  8002  seqomlem2  8383  xpf1o  9070  aceq0  10031  dfac5  10042  zfac  10373  zfcndrep  10528  zfcndac  10533  ltasr  11014  axpre-ltadd  11081  absmod0  15256  absz  15264  smuval2  16442  prmdvdsexp  16676  isacs2  17610  isacs1i  17614  mreacs  17615  abvfval  20778  abvpropd  20803  isclo2  23063  t0sep  23299  kqt0lem  23711  r0sep  23723  iccpnfcnv  24921  rolle  25967  2sqreultlem  27424  2sqreunnltlem  27427  tgjustr  28556  wlkeq  29717  eigre  31921  fgreu  32759  fcnvgreu  32760  gsumhashmul  33143  xrge0iifcnv  34093  axsepg2  35241  axsepg2ALT  35242  cvmlift2lem13  35513  iota5f  35922  nn0prpwlem  36520  nn0prpw  36521  bj-zfauscl  37247  bj-axseprep  37397  bj-axreprepsep  37398  wl-eudf  37911  ismndo2  38209  islaut  40543  ispautN  40559  mrefg2  43153  zindbi  43392  jm2.19lem3  43437  oaordnr  43742  omnord1  43751  oenord1  43762  alephiso2  44003  ntrneiel2  44531  ntrneik4  44546  iotavalb  44875  eusnsn  47486  aiota0def  47556  fargshiftfo  47914  isuspgrimlem  48383  line2x  49242  eufsnlem  49328  thincciso  49940  thinccisod  49941  termcarweu  50015