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  2516  axext3  2633  axext3ALT  2634  bm1.1  2636  eqeq1dALT  2654  pm13.183  3376  elabgt  3379  elrab3t  3395  mob  3421  reu6  3428  sbctt  3533  sbcabel  3550  isoeq2  6608  caovcang  6877  domunfican  8274  axacndlem4  9470  axacnd  9472  expeq0  12930  dfrtrclrec2  13841  relexpind  13848  sumodd  15158  prmdvdsexp  15474  isacs  16359  acsfn  16367  tsrlemax  17267  odeq  18015  isslw  18069  isabv  18867  t0sep  21176  xkopt  21506  kqt0lem  21587  r0sep  21599  nrmr0reg  21600  ismet  22175  isxmet  22176  stdbdxmet  22367  xrsxmet  22659  iccpnfcnv  22790  mdegle0  23882  isppw2  24886  eleclclwwlkn  27040  eupth2lem1  27196  hvaddcan  28055  eigre  28822  xrge0iifcnv  30107  sgn0bi  30737  signswch  30766  bnj1468  31042  br1steqgOLD  31798  br2ndeqgOLD  31799  subtr2  32434  nn0prpwlem  32442  nn0prpw  32443  bj-axext3  32894  dfgcd3  33300  ftc1anclem6  33620  zindbi  37828  expdioph  37907  islssfg2  37958  eliunov2  38288  pm14.122b  38941
 Copyright terms: Public domain W3C validator