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  2709  axextmo  2711  eqeq1dALT  2739  pm13.183  3616  elabgtOLD  3623  elrab3t  3642  mob  3673  reu6  3682  sbctt  3813  sbcabel  3832  isoeq2  7259  caovcang  7551  domunfican  9260  axacndlem4  10542  axacnd  10544  expeq0  13990  dfrtrclrec2  14935  relexpind  14941  sumodd  16262  prmdvdsexp  16583  isacs  17523  acsfn  17531  tsrlemax  18467  odeq  19323  isslw  19381  isabv  20263  t0sep  22659  xkopt  22990  kqt0lem  23071  r0sep  23083  nrmr0reg  23084  ismet  23660  isxmet  23661  stdbdxmet  23855  xrsxmet  24156  iccpnfcnv  24291  mdegle0  25426  isppw2  26448  tgjustf  27301  eleclclwwlkn  28906  eupth2lem1  29048  hvaddcan  29898  eigre  30663  opsbc2ie  31290  xrge0iifcnv  32383  sgn0bi  33016  signswch  33042  bnj1468  33327  subtr2  34754  nn0prpwlem  34761  nn0prpw  34762  bj-bm1.3ii  35502  dfgcd3  35762  ftc1anclem6  36123  zindbi  41208  expdioph  41285  islssfg2  41336  eliunov2  41893  pm14.122b  42645  elsetpreimafvbi  45515  line2ylem  46769  line2xlem  46771
  Copyright terms: Public domain W3C validator