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  3688  sbc2or  3751  axrep1  5227  axreplem  5228  zfrepclf  5238  axsepg  5244  zfauscl  5245  notzfaus  5310  copsexgw  5446  copsexg  5447  euotd  5469  cnveq0  6163  iota5  6483  eufnfv  7185  isoeq1  7273  isoeq3  7275  isores2  7289  isores3  7291  isotr  7292  isoini2  7295  riota5f  7353  caovordg  7575  caovord  7579  dfoprab4f  8010  seqomlem2  8392  xpf1o  9079  aceq0  10040  dfac5  10051  zfac  10382  zfcndrep  10537  zfcndac  10542  ltasr  11023  axpre-ltadd  11090  absmod0  15238  absz  15246  smuval2  16421  prmdvdsexp  16654  isacs2  17588  isacs1i  17592  mreacs  17593  abvfval  20755  abvpropd  20780  isclo2  23044  t0sep  23280  kqt0lem  23692  r0sep  23704  iccpnfcnv  24910  rolle  25962  2sqreultlem  27426  2sqreunnltlem  27429  tgjustr  28558  wlkeq  29719  eigre  31922  fgreu  32760  fcnvgreu  32761  gsumhashmul  33160  xrge0iifcnv  34110  axsepg2  35257  axsepg2ALT  35258  cvmlift2lem13  35528  iota5f  35937  nn0prpwlem  36535  nn0prpw  36536  bj-zfauscl  37166  bj-axseprep  37316  bj-axreprepsep  37317  wl-eudf  37821  ismndo2  38119  islaut  40453  ispautN  40469  mrefg2  43058  zindbi  43297  jm2.19lem3  43342  oaordnr  43647  omnord1  43656  oenord1  43667  alephiso2  43908  ntrneiel2  44436  ntrneik4  44451  iotavalb  44780  eusnsn  47380  aiota0def  47450  fargshiftfo  47796  isuspgrimlem  48249  line2x  49108  eufsnlem  49194  thincciso  49806  thinccisod  49807  termcarweu  49881