MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2d Structured version   Visualization version   GIF version

Theorem bibi2d 331
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
StepHypRef Expression
1 imbid.1 . . . . 5 (𝜑 → (𝜓𝜒))
21pm5.74i 260 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 326 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 259 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 259 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 292 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 261 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  bibi1d  332  bibi12d  334  biantr  992  bimsc1  999  eujust  2500  eujustALT  2501  euf  2506  reu6i  3430  sbc2or  3477  axrep1  4805  axrep2  4806  axrep3  4807  zfrepclf  4810  axsep2  4815  zfauscl  4816  copsexg  4985  euotd  5004  cnveq0  5626  iotaval  5900  iota5  5909  eufnfv  6531  isoeq1  6607  isoeq3  6609  isores2  6623  isores3  6625  isotr  6626  isoini2  6629  riota5f  6676  caovordg  6883  caovord  6887  dfoprab4f  7270  seqomlem2  7591  xpf1o  8163  aceq0  8979  dfac5  8989  zfac  9320  zfcndrep  9474  zfcndac  9479  ltasr  9959  axpre-ltadd  10026  absmod0  14087  absz  14095  smuval2  15251  prmdvdsexp  15474  isacs2  16361  isacs1i  16365  mreacs  16366  abvfval  18866  abvpropd  18890  isclo2  20940  t0sep  21176  kqt0lem  21587  r0sep  21599  iccpnfcnv  22790  rolle  23798  wlkeq  26585  eigre  28822  fgreu  29599  fcnvgreu  29600  xrge0iifcnv  30107  cvmlift2lem13  31423  iota5f  31732  nn0prpwlem  32442  nn0prpw  32443  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-axsep2  33046  wl-eudf  33484  ismndo2  33803  islaut  35687  ispautN  35703  mrefg2  37587  zindbi  37828  jm2.19lem3  37875  ntrneiel2  38701  ntrneik4  38716  iotavalb  38948  fargshiftfo  41703
  Copyright terms: Public domain W3C validator