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  805  eujust  2574  eujustALT  2575  euf  2579  reu6i  3750  sbc2or  3813  axrep1  5304  axreplem  5305  zfrepclf  5312  axsepg  5318  zfauscl  5319  notzfaus  5381  copsexgw  5510  copsexg  5511  euotd  5532  cnveq0  6228  iotavalOLD  6547  iota5  6556  eufnfv  7266  isoeq1  7353  isoeq3  7355  isores2  7369  isores3  7371  isotr  7372  isoini2  7375  riota5f  7433  caovordg  7657  caovord  7661  dfoprab4f  8097  seqomlem2  8507  xpf1o  9205  aceq0  10187  dfac5  10198  zfac  10529  zfcndrep  10683  zfcndac  10688  ltasr  11169  axpre-ltadd  11236  absmod0  15352  absz  15360  smuval2  16528  prmdvdsexp  16762  isacs2  17711  isacs1i  17715  mreacs  17716  abvfval  20833  abvpropd  20858  isclo2  23117  t0sep  23353  kqt0lem  23765  r0sep  23777  iccpnfcnv  24994  rolle  26048  2sqreultlem  27509  2sqreunnltlem  27512  tgjustr  28500  wlkeq  29670  eigre  31867  fgreu  32690  fcnvgreu  32691  gsumhashmul  33040  xrge0iifcnv  33879  axsepg2  35058  axsepg2ALT  35059  cvmlift2lem13  35283  iota5f  35686  nn0prpwlem  36288  nn0prpw  36289  bj-zfauscl  36890  wl-eudf  37526  ismndo2  37834  islaut  40040  ispautN  40056  mrefg2  42663  zindbi  42903  jm2.19lem3  42948  oaordnr  43258  omnord1  43267  oenord1  43278  alephiso2  43520  ntrneiel2  44048  ntrneik4  44063  iotavalb  44399  eusnsn  46941  aiota0def  47011  fargshiftfo  47316  isuspgrimlem  47758  line2x  48488  eufsnlem  48554  thincciso  48716