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  2952  uneq1  3335  r19.45zv  3564  rexprg  3696  rextpg  3698  swopolem  4339  ordsseleq  4437  cantnflem1  7407  axgroth2  8463  axgroth3  8469  lelttric  8943  ltxr  10473  xmulneg1  10605  fzpr  10856  elfzp12  10877  caubnd  11858  isprm6  12804  vdwlem10  13053  irredmul  15507  domneq0  16054  opsrval  16232  znfld  16530  logreclem  20132  perfectlem2  20485  h1datom  22177  xrlelttric  23265  esumpcvgval  23461  nofulllem5  24431  segcon2  24800  pridl  26765  ismaxidl  26768  ispridlc  26798  pridlc  26799  dmnnzd  26803  sbc3org  28594  4atlem3a  30408  pmapjoin  30663  lcfl3  32306  lcfl4N  32307
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