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

Theorem orbi1d 683
Description: Deduction adding a right 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
orbi1d  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )

Proof of Theorem orbi1d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi2d 682 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 376 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 376 . 2  |-  ( ( ch  \/  th )  <->  ( th  \/  ch )
)
52, 3, 43bitr4g 279 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357
This theorem is referenced by:  orbi1  686  orbi12d  690  eueq2  2939  uneq1  3322  r19.45zv  3551  rexprg  3683  rextpg  3685  swopolem  4323  ordsseleq  4421  cantnflem1  7391  axgroth2  8447  axgroth3  8453  lelttric  8927  ltxr  10457  xmulneg1  10589  fzpr  10840  elfzp12  10861  caubnd  11842  isprm6  12788  vdwlem10  13037  irredmul  15491  domneq0  16038  opsrval  16216  znfld  16514  logreclem  20116  perfectlem2  20469  h1datom  22161  nofulllem5  23771  segcon2  24139  pridl  26074  ismaxidl  26077  ispridlc  26107  pridlc  26108  dmnnzd  26112  sbc3org  27668  4atlem3a  29159  pmapjoin  29414  lcfl3  31057  lcfl4N  31058
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