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

Theorem orbi1d 684
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 683 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 377 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 377 . 2  |-  ( ( ch  \/  th )  <->  ( th  \/  ch )
)
52, 3, 43bitr4g 280 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358
This theorem is referenced by:  orbi1  687  orbi12d  691  eueq2  3044  uneq1  3430  r19.45zv  3661  rexprg  3794  rextpg  3796  swopolem  4446  ordsseleq  4544  cantnflem1  7571  axgroth2  8626  axgroth3  8632  lelttric  9106  ltxr  10640  xmulneg1  10773  fzpr  11026  elfzp12  11049  caubnd  12082  isprm6  13029  vdwlem10  13278  irredmul  15734  domneq0  16277  opsrval  16455  znfld  16757  logreclem  20520  perfectlem2  20874  h1datom  22925  xrlelttric  23950  esumpcvgval  24257  nofulllem5  25377  segcon2  25746  pridl  26331  ismaxidl  26334  ispridlc  26364  pridlc  26365  dmnnzd  26369  sbc3org  27952  4atlem3a  29762  pmapjoin  30017  lcfl3  31660  lcfl4N  31661
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