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  2571  eujustALT  2572  euf  2576  reu6i  3674  sbc2or  3737  axrep1  5213  axreplem  5214  zfrepclf  5226  axsepg  5232  zfauscl  5233  exnelv  5248  notzfaus  5305  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  euotd  5467  cnveq0  6161  iota5  6481  eufnfv  7184  isoeq1  7272  isoeq3  7274  isores2  7288  isores3  7290  isotr  7291  isoini2  7294  riota5f  7352  caovordg  7574  caovord  7578  dfoprab4f  8009  seqomlem2  8390  xpf1o  9077  aceq0  10040  dfac5  10051  zfac  10382  zfcndrep  10537  zfcndac  10542  ltasr  11023  axpre-ltadd  11090  absmod0  15265  absz  15273  smuval2  16451  prmdvdsexp  16685  isacs2  17619  isacs1i  17623  mreacs  17624  abvfval  20787  abvpropd  20812  isclo2  23053  t0sep  23289  kqt0lem  23701  r0sep  23713  iccpnfcnv  24911  rolle  25957  2sqreultlem  27410  2sqreunnltlem  27413  tgjustr  28542  wlkeq  29702  eigre  31906  fgreu  32744  fcnvgreu  32745  gsumhashmul  33128  xrge0iifcnv  34077  axsepg2  35225  axsepg2ALT  35226  cvmlift2lem13  35497  iota5f  35906  nn0prpwlem  36504  nn0prpw  36505  bj-zfauscl  37231  bj-axseprep  37381  bj-axreprepsep  37382  wl-eudf  37897  ismndo2  38195  islaut  40529  ispautN  40545  mrefg2  43139  zindbi  43374  jm2.19lem3  43419  oaordnr  43724  omnord1  43733  oenord1  43744  alephiso2  43985  ntrneiel2  44513  ntrneik4  44528  iotavalb  44857  eusnsn  47474  aiota0def  47544  fargshiftfo  47902  isuspgrimlem  48371  line2x  49230  eufsnlem  49316  thincciso  49928  thinccisod  49929  termcarweu  50003