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  1398  eueq2  3015  sbc2or  3075  rexprg  3759  rextpg  3761  swopolem  4402  elsucg  4538  elsuc2g  4539  poleloe  5156  brdifun  6771  brwdom  7368  isfin1a  8005  elgch  8331  suplem2pr  8764  axlttri  8981  elznn0  10127  elznn  10128  zindd  10202  rpneg  10472  dfle2  10570  fzosplitsni  11010  bitsf1  12728  isprm6  12879  infpn2  13051  irredmul  15584  domneq0  16131  znfld  16614  quotval  19770  plydivlem4  19774  plydivex  19775  aalioulem2  19811  aalioulem5  19814  aalioulem6  19815  aaliou  19816  aaliou2  19818  aaliou2b  19819  eliccioo  23382  ballotlemfc0  23999  ballotlemfcc  24000  mulcan1g  24490  axcontlem7  25157  seglelin  25298  lineunray  25329  pridl  25985  maxidlval  25987  ispridlc  26018  pridlc  26019  dmnnzd  26023  aomclem8  26482  hashv01gt1  27482  orbi1r  27999  lcfl7N  31743
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