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  1441  eueq2  3216  sbc2or  3279  rexprg  4010  rextpg  4012  swopolem  4734  elsucg  4870  elsuc2g  4871  poleloe  5316  brdifun  7214  brwdom  7869  isfin1a  8548  elgch  8876  suplem2pr  9309  axlttri  9533  mulcan1g  10076  elznn0  10748  elznn  10749  zindd  10830  rpneg  11107  dfle2  11211  fzosplitsni  11721  hashv01gt1  12203  bitsf1  13730  isprm6  13883  infpn2  14062  irredmul  16893  domneq0  17461  znfld  18088  quotval  21860  plydivlem4  21864  plydivex  21865  aalioulem2  21901  aalioulem5  21904  aalioulem6  21905  aaliou  21906  aaliou2  21908  aaliou2b  21909  axcontlem7  23337  eliccioo  26226  tlt2  26245  sibfof  26846  ballotlemfc0  26995  ballotlemfcc  26996  seglelin  28267  lineunray  28298  mblfinlem2  28553  pridl  28961  maxidlval  28963  ispridlc  28994  pridlc  28995  dmnnzd  28999  aomclem8  29538  hashecclwwlkn1  30632  lindslinindsimp2lem5  31089  lindslinindsimp2  31090  orbi1r  31496  lcfl7N  35428
  Copyright terms: Public domain W3C validator