Theorem bibi2d 345

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 274	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 340	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 306	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 275	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi1d  346  bibi12d  348  biantr  817  eujust  2601  eujustALT  2602  euf  2606  reu6i  3694  sbc2or  3756  axrep1  5233  axreplem  5234  zfrepclf  5246  axsepg  5252  zfauscl  5253  exnelv  5268  notzfaus  5325  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  euotd  5487  cnveq0  6188  iota5  6508  eufnfv  7217  isoeq1  7305  isoeq3  7307  isores2  7321  isores3  7323  isotr  7324  isoini2  7327  riota5f  7385  caovordg  7607  caovord  7611  dfoprab4f  8041  seqomlem2  8426  xpf1o  9115  elirrv  9547  aceq0  10090  dfac5  10100  zfac  10432  zfcndrep  10587  zfcndac  10592  ltasr  11073  axpre-ltadd  11140  absmod0  15344  absz  15352  smuval2  16530  prmdvdsexp  16764  isacs2  17699  isacs1i  17703  mreacs  17704  abvfval  20882  abvpropd  20907  isclo2  23206  t0sep  23442  kqt0lem  23854  r0sep  23866  iccpnfcnv  25064  rolle  26110  2sqreultlem  27569  2sqreunnltlem  27572  tgjustr  28701  wlkeq  29892  eigre  32096  fgreu  32928  fcnvgreu  32929  gsumhashmul  33300  xrge0iifcnv  34240  axsepg2  35448  axsepg3  35449  axsepg3ALT  35450  axsepg4  35451  axsepg5  35452  cvmlift2lem13  35678  iota5f  36087  nn0prpwlem  36695  nn0prpw  36696  bj-zfauscl  37421  bj-axseprep  37571  bj-axreprepsep  37572  wl-eudf  38087  ismndo2  38385  islaut  40719  ispautN  40735  mrefg2  43300  zindbi  43535  jm2.19lem3  43580  oaordnr  43885  omnord1  43894  oenord1  43905  alephiso2  44146  ntrneiel2  44674  ntrneik4  44689  iotavalb  45004  eusnsn  47618  aiota0def  47688  fargshiftfo  48046  isuspgrimlem  48515  line2x  49385  eufsnlem  49470  thincciso  50082  thinccisod  50083  termcarweu  50157