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

Theorem bibi1d 332
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
bibi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem bibi1d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi2d 331 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 212 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 212 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 303 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:  bibi12d  334  bibi1  340  biass  373  eubid  2625  axext3  2742  axext3ALT  2743  bm1.1  2745  eqeq1dALT  2763  pm13.183  3484  elabgt  3487  elrab3t  3503  mob  3529  reu6  3536  sbctt  3641  sbcabel  3658  isoeq2  6731  caovcang  7000  domunfican  8398  axacndlem4  9624  axacnd  9626  expeq0  13084  dfrtrclrec2  13996  relexpind  14003  sumodd  15313  prmdvdsexp  15629  isacs  16513  acsfn  16521  tsrlemax  17421  odeq  18169  isslw  18223  isabv  19021  t0sep  21330  xkopt  21660  kqt0lem  21741  r0sep  21753  nrmr0reg  21754  ismet  22329  isxmet  22330  stdbdxmet  22521  xrsxmet  22813  iccpnfcnv  22944  mdegle0  24036  isppw2  25040  eleclclwwlkn  27207  eupth2lem1  27370  hvaddcan  28236  eigre  29003  xrge0iifcnv  30288  sgn0bi  30918  signswch  30947  bnj1468  31223  br1steqgOLD  31979  br2ndeqgOLD  31980  subtr2  32615  nn0prpwlem  32623  nn0prpw  32624  bj-axext3  33075  dfgcd3  33481  ftc1anclem6  33803  zindbi  38013  expdioph  38092  islssfg2  38143  eliunov2  38473  pm14.122b  39126
  Copyright terms: Public domain W3C validator