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  3282  uneq1  3656  r19.45zv  3931  rexprg  4083  rextpg  4085  swopolem  4815  ordsseleq  4913  cantnflem1  8120  cantnflem1OLD  8143  axgroth2  9215  axgroth3  9221  lelttric  9703  ltxr  11336  xmulneg1  11473  fzpr  11747  elfzp12  11769  caubnd  13171  isprm6  14126  vdwlem10  14384  irredmul  17230  domneq0  17816  opsrval  18009  znfld  18468  logreclem  23016  perfectlem2  23371  legov3  23849  colperpex  23952  lmif  23975  islmib  23977  friendshipgt3  24945  h1datom  26323  xrlelttric  27395  tlt3  27477  esumpcvgval  27909  sibfof  28107  nofulllem5  29393  segcon2  29682  cnambfre  29990  pridl  30361  ismaxidl  30364  ispridlc  30394  pridlc  30395  dmnnzd  30399  lcmval  31122  lcmass  31142  fourierdlem80  31810  lindslinindsimp2  32546  sbc3orgOLD  32783  4atlem3a  34794  pmapjoin  35049  lcfl3  36692  lcfl4N  36693
  Copyright terms: Public domain W3C validator