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  3257  uneq1  3633  r19.45zv  3908  rexprg  4060  rextpg  4062  swopolem  4795  ordsseleq  4893  cantnflem1  8106  cantnflem1OLD  8129  axgroth2  9201  axgroth3  9207  lelttric  9689  ltxr  11328  xmulneg1  11465  fzpr  11739  elfzp12  11761  caubnd  13165  isprm6  14122  vdwlem10  14380  irredmul  17226  domneq0  17814  opsrval  18007  znfld  18466  logreclem  23015  perfectlem2  23370  legov3  23849  colperpex  23972  lmif  24016  islmib  24018  friendshipgt3  24986  h1datom  26365  xrlelttric  27437  tlt3  27519  esumpcvgval  27950  sibfof  28148  nofulllem5  29434  segcon2  29723  cnambfre  30031  pridl  30402  ismaxidl  30405  ispridlc  30435  pridlc  30436  dmnnzd  30440  lcmval  31167  lcmass  31187  fourierdlem80  31854  lindslinindsimp2  32774  sbc3orgOLD  33011  4atlem3a  35023  pmapjoin  35278  lcfl3  36923  lcfl4N  36924
  Copyright terms: Public domain W3C validator