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

Theorem orbi1d 702
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-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 701 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 387 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 387 . 2  |-  ( ( ch  \/  th )  <->  ( th  \/  ch )
)
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
This theorem is referenced by:  orbi1  705  orbi12d  709  eueq2  3154  uneq1  3524  r19.45zv  3798  rexprg  3947  rextpg  3949  swopolem  4671  ordsseleq  4769  cantnflem1  7918  cantnflem1OLD  7941  axgroth2  9013  axgroth3  9019  lelttric  9502  ltxr  11116  xmulneg1  11253  fzpr  11532  elfzp12  11560  caubnd  12867  isprm6  13816  vdwlem10  14072  irredmul  16823  domneq0  17391  opsrval  17578  znfld  18015  logreclem  22236  perfectlem2  22591  h1datom  25007  xrlelttric  26067  tlt3  26148  esumpcvgval  26549  sibfof  26748  nofulllem5  27869  segcon2  28158  cnambfre  28466  pridl  28863  ismaxidl  28866  ispridlc  28896  pridlc  28897  dmnnzd  28901  friendshipgt3  30740  lindslinindsimp2  30994  sbc3orgOLD  31334  4atlem3a  33337  pmapjoin  33592  lcfl3  35235  lcfl4N  35236
  Copyright terms: Public domain W3C validator