MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi2d Unicode version

Theorem orbi2d 682
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
orbi2d  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )

Proof of Theorem orbi2d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21imbi2d 307 . 2  |-  ( ph  ->  ( ( -.  th  ->  ps )  <->  ( -.  th 
->  ch ) ) )
3 df-or 359 . 2  |-  ( ( th  \/  ps )  <->  ( -.  th  ->  ps ) )
4 df-or 359 . 2  |-  ( ( th  \/  ch )  <->  ( -.  th  ->  ch ) )
52, 3, 43bitr4g 279 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357
This theorem is referenced by:  orbi1d  683  orbi12d  690  cad1  1388  eueq2  2939  sbc2or  2999  rexprg  3683  rextpg  3685  swopolem  4323  elsucg  4459  elsuc2g  4460  poleloe  5077  brdifun  6687  brwdom  7281  isfin1a  7918  elgch  8244  suplem2pr  8677  axlttri  8894  elznn0  10038  elznn  10039  zindd  10113  rpneg  10383  dfle2  10481  fzosplitsni  10921  bitsf1  12637  isprm6  12788  infpn2  12960  irredmul  15491  domneq0  16038  znfld  16514  quotval  19672  plydivlem4  19676  plydivex  19677  aalioulem2  19713  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou2  19720  aaliou2b  19721  ballotlemfc0  23051  ballotlemfcc  23052  eliccioo  23115  mulcan1g  24084  axcontlem7  24598  seglelin  24739  lineunray  24770  vtarsuelt  25895  pridl  26662  maxidlval  26664  ispridlc  26695  pridlc  26696  dmnnzd  26700  aomclem8  27159  orbi1r  28271  lcfl7N  31691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator