MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi1d Structured version   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  3100  uneq1  3486  r19.45zv  3717  rexprg  3850  rextpg  3852  swopolem  4504  ordsseleq  4602  cantnflem1  7637  axgroth2  8692  axgroth3  8698  lelttric  9172  ltxr  10707  xmulneg1  10840  fzpr  11093  elfzp12  11118  caubnd  12154  isprm6  13101  vdwlem10  13350  irredmul  15806  domneq0  16349  opsrval  16527  znfld  16833  logreclem  20652  perfectlem2  21006  h1datom  23076  xrlelttric  24110  esumpcvgval  24460  sibfof  24646  nofulllem5  25653  segcon2  26031  cnambfre  26245  pridl  26638  ismaxidl  26641  ispridlc  26671  pridlc  26672  dmnnzd  26676  sbc3org  28553  4atlem3a  30331  pmapjoin  30586  lcfl3  32229  lcfl4N  32230
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