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

Theorem orbi2d 701
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-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 316 . 2  |-  ( ph  ->  ( ( -.  th  ->  ps )  <->  ( -.  th 
->  ch ) ) )
3 df-or 370 . 2  |-  ( ( th  \/  ps )  <->  ( -.  th  ->  ps ) )
4 df-or 370 . 2  |-  ( ( th  \/  ch )  <->  ( -.  th  ->  ch ) )
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  orbi1d  702  orbi12d  709  cad1  1450  eueq2  3277  sbc2or  3340  rexprg  4077  rextpg  4079  swopolem  4809  elsucg  4945  elsuc2g  4946  poleloe  5399  brdifun  7335  brwdom  7989  isfin1a  8668  elgch  8996  suplem2pr  9427  axlttri  9652  mulcan1g  10198  elznn0  10875  elznn  10876  zindd  10958  rpneg  11245  dfle2  11349  fzosplitsni  11884  hashv01gt1  12382  bitsf1  13951  isprm6  14105  infpn2  14286  irredmul  17142  domneq0  17717  znfld  18366  quotval  22422  plydivlem4  22426  plydivex  22427  aalioulem2  22463  aalioulem5  22466  aalioulem6  22467  aaliou  22468  aaliou2  22470  aaliou2b  22471  axcontlem7  23949  hashecclwwlkn1  24510  eliccioo  27295  tlt2  27314  sibfof  27922  ballotlemfc0  28071  ballotlemfcc  28072  seglelin  29343  lineunray  29374  mblfinlem2  29629  pridl  30037  maxidlval  30039  ispridlc  30070  pridlc  30071  dmnnzd  30075  aomclem8  30611  lcmval  30798  lcmneg  30809  lcmass  30818  lindslinindsimp2lem5  32136  lindslinindsimp2  32137  orbi1r  32358  lcfl7N  36298
  Copyright terms: Public domain W3C validator