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

Theorem bibi1d 343
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 342 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 221 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 221 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 313 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  bibi12d  345  bibi1  351  biass  385  axextg  2710  axextmo  2712  eqeq1dALT  2740  pm13.183  3616  elabgtOLD  3623  elrab3t  3642  mob  3673  reu6  3682  sbctt  3813  sbcabel  3832  isoeq2  7259  caovcang  7549  domunfican  9222  axacndlem4  10504  axacnd  10506  expeq0  13952  dfrtrclrec2  14903  relexpind  14909  sumodd  16230  prmdvdsexp  16551  isacs  17491  acsfn  17499  tsrlemax  18435  odeq  19291  isslw  19349  isabv  20231  t0sep  22627  xkopt  22958  kqt0lem  23039  r0sep  23051  nrmr0reg  23052  ismet  23628  isxmet  23629  stdbdxmet  23823  xrsxmet  24124  iccpnfcnv  24259  mdegle0  25394  isppw2  26416  tgjustf  27244  eleclclwwlkn  28849  eupth2lem1  28991  hvaddcan  29841  eigre  30606  opsbc2ie  31233  xrge0iifcnv  32326  sgn0bi  32959  signswch  32985  bnj1468  33270  subtr2  34725  nn0prpwlem  34732  nn0prpw  34733  bj-bm1.3ii  35473  dfgcd3  35733  ftc1anclem6  36094  zindbi  41179  expdioph  41256  islssfg2  41307  eliunov2  41862  pm14.122b  42614  elsetpreimafvbi  45484  line2ylem  46738  line2xlem  46740
  Copyright terms: Public domain W3C validator