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

Theorem orbi2d 684
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 309 . 2  |-  ( ph  ->  ( ( -.  th  ->  ps )  <->  ( -.  th 
->  ch ) ) )
3 df-or 361 . 2  |-  ( ( th  \/  ps )  <->  ( -.  th  ->  ps ) )
4 df-or 361 . 2  |-  ( ( th  \/  ch )  <->  ( -.  th  ->  ch ) )
52, 3, 43bitr4g 281 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359
This theorem is referenced by:  orbi1d  685  orbi12d  692  cad1  1408  eueq2  3114  sbc2or  3175  rexprg  3882  rextpg  3884  swopolem  4541  elsucg  4677  elsuc2g  4678  poleloe  5297  brdifun  6961  brwdom  7564  isfin1a  8203  elgch  8528  suplem2pr  8961  axlttri  9178  elznn0  10327  elznn  10328  zindd  10402  rpneg  10672  dfle2  10771  fzosplitsni  11227  hashv01gt1  11660  bitsf1  12989  isprm6  13140  infpn2  13312  irredmul  15845  domneq0  16388  znfld  16872  quotval  20240  plydivlem4  20244  plydivex  20245  aalioulem2  20281  aalioulem5  20284  aalioulem6  20285  aaliou  20286  aaliou2  20288  aaliou2b  20289  eliccioo  24208  sibfof  24685  ballotlemfc0  24781  ballotlemfcc  24782  mulcan1g  25220  axcontlem7  25940  seglelin  26081  lineunray  26112  mblfinlem2  26280  pridl  26685  maxidlval  26687  ispridlc  26718  pridlc  26719  dmnnzd  26723  aomclem8  27174  orbi1r  28690  lcfl7N  32397
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 179  df-or 361
  Copyright terms: Public domain W3C validator