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  1453  eueq2  3259  sbc2or  3322  rexprg  4064  rextpg  4066  swopolem  4799  elsucg  4935  elsuc2g  4936  poleloe  5391  brdifun  7340  brwdom  7996  isfin1a  8675  elgch  9003  suplem2pr  9434  axlttri  9659  mulcan1g  10209  elznn0  10886  elznn  10887  zindd  10972  rpneg  11260  dfle2  11364  fzosplitsni  11902  hashv01gt1  12400  bitsf1  14078  isprm6  14232  infpn2  14413  irredmul  17337  domneq0  17925  znfld  18577  quotval  22666  plydivlem4  22670  plydivex  22671  aalioulem2  22707  aalioulem5  22710  aalioulem6  22711  aaliou  22712  aaliou2  22714  aaliou2b  22715  axcontlem7  24251  hashecclwwlkn1  24812  eliccioo  27605  tlt2  27630  sibfof  28260  ballotlemfc0  28409  ballotlemfcc  28410  seglelin  29742  lineunray  29773  mblfinlem2  30028  pridl  30410  maxidlval  30412  ispridlc  30443  pridlc  30444  dmnnzd  30448  aomclem8  30983  lcmval  31174  lcmneg  31185  lcmass  31194  lindslinindsimp2lem5  32933  lindslinindsimp2  32934  orbi1r  33147  lcfl7N  37103
  Copyright terms: Public domain W3C validator