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 259 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 326 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 258 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 258 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 291 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 260 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  bibi1d  332  bibi12d  334  biantr  968  bimsc1  976  eujust  2460  eujustALT  2461  euf  2466  reu6i  3364  sbc2or  3411  axrep1  4695  axrep2  4696  axrep3  4697  zfrepclf  4700  axsep2  4705  zfauscl  4706  copsexg  4876  euotd  4891  cnveq0  5495  iotaval  5765  iota5  5774  eufnfv  6373  isoeq1  6445  isoeq3  6447  isores2  6461  isores3  6463  isotr  6464  isoini2  6467  riota5f  6513  caovordg  6717  caovord  6721  dfoprab4f  7095  seqomlem2  7411  xpf1o  7985  aceq0  8802  dfac5  8812  zfac  9143  zfcndrep  9293  zfcndac  9298  ltasr  9778  axpre-ltadd  9845  absmod0  13840  absz  13848  smuval2  14991  prmdvdsexp  15214  isacs2  16086  isacs1i  16090  mreacs  16091  abvfval  18590  abvpropd  18614  isclo2  20650  t0sep  20886  kqt0lem  21297  r0sep  21309  iccpnfcnv  22499  rolle  23502  fargshiftfo  25960  2wlkeq  26029  eigre  27872  fgreu  28648  fcnvgreu  28649  xrge0iifcnv  29101  cvmlift2lem13  30345  iota5f  30655  nn0prpwlem  31281  nn0prpw  31282  bj-axrep1  31770  bj-axrep2  31771  bj-axrep3  31772  bj-axsep2  31907  wl-eudf  32327  ismndo2  32637  islaut  34181  ispautN  34197  mrefg2  36082  zindbi  36323  jm2.19lem3  36370  ntrneiel2  37198  ntrneik4  37213  iotavalb  37447  1wlkeq  40830
  Copyright terms: Public domain W3C validator