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

Theorem bibi2d 333
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 262 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 328 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 261 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 261 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 294 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 263 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  bibi1d  334  bibi12d  336  biantr  840  bimsc1  870  eujust  2587  eujustALT  2588  euf  2600  eufOLD  2601  reu6i  3558  sbc2or  3607  axrep1  4933  axreplem  4934  zfrepclf  4939  axsep2  4944  zfauscl  4945  copsexg  5113  euotd  5136  cnveq0  5776  iotaval  6044  iota5  6053  eufnfv  6688  isoeq1  6763  isoeq3  6765  isores2  6779  isores3  6781  isotr  6782  isoini2  6785  riota5f  6832  caovordg  7043  caovord  7047  dfoprab4f  7430  seqomlem2  7754  xpf1o  8333  aceq0  9196  dfac5  9206  zfac  9539  zfcndrep  9693  zfcndac  9698  ltasr  10178  axpre-ltadd  10245  absmod0  14342  absz  14350  smuval2  15499  prmdvdsexp  15720  isacs2  16593  isacs1i  16597  mreacs  16598  abvfval  19101  abvpropd  19125  isclo2  21186  t0sep  21422  kqt0lem  21833  r0sep  21845  iccpnfcnv  23036  rolle  24058  wlkeq  26834  eigre  29171  fgreu  29941  fcnvgreu  29942  xrge0iifcnv  30447  cvmlift2lem13  31766  iota5f  32073  nn0prpwlem  32781  nn0prpw  32782  bj-axrep1  33239  bj-axrep2  33240  bj-axrep3  33241  bj-axsep2  33369  bj-zfauscl  33370  wl-eudf  33800  ismndo2  34116  islaut  36060  ispautN  36076  mrefg2  37972  zindbi  38212  jm2.19lem3  38259  ntrneiel2  39082  ntrneik4  39097  iotavalb  39328  eusnsn  41832  aiota0def  41861  fargshiftfo  42136
  Copyright terms: Public domain W3C validator