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

Theorem orbi2d 683
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 308 . 2  |-  ( ph  ->  ( ( -.  th  ->  ps )  <->  ( -.  th 
->  ch ) ) )
3 df-or 360 . 2  |-  ( ( th  \/  ps )  <->  ( -.  th  ->  ps ) )
4 df-or 360 . 2  |-  ( ( th  \/  ch )  <->  ( -.  th  ->  ch ) )
52, 3, 43bitr4g 280 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358
This theorem is referenced by:  orbi1d  684  orbi12d  691  cad1  1404  eueq2  3076  sbc2or  3137  rexprg  3826  rextpg  3828  swopolem  4480  elsucg  4616  elsuc2g  4617  poleloe  5235  brdifun  6899  brwdom  7499  isfin1a  8136  elgch  8461  suplem2pr  8894  axlttri  9111  elznn0  10260  elznn  10261  zindd  10335  rpneg  10605  dfle2  10704  fzosplitsni  11159  hashv01gt1  11592  bitsf1  12921  isprm6  13072  infpn2  13244  irredmul  15777  domneq0  16320  znfld  16804  quotval  20170  plydivlem4  20174  plydivex  20175  aalioulem2  20211  aalioulem5  20214  aalioulem6  20215  aaliou  20216  aaliou2  20218  aaliou2b  20219  eliccioo  24138  sibfof  24615  ballotlemfc0  24711  ballotlemfcc  24712  mulcan1g  25150  axcontlem7  25821  seglelin  25962  lineunray  25993  mblfinlem  26151  pridl  26545  maxidlval  26547  ispridlc  26578  pridlc  26579  dmnnzd  26583  aomclem8  27035  orbi1r  28311  lcfl7N  31996
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 178  df-or 360
  Copyright terms: Public domain W3C validator