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

Theorem orbi1i 507
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
orbi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
orbi1i  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 377 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 506 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 377 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 263 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  orbi12i  508  orordi  517  jaoi2  934  3anor  950  3or6  1265  19.45  1899  unass  3496  tz7.48lem  6690  dffin7-2  8270  zorng  8376  entri2  8425  grothprim  8701  leloe  9153  arch  10210  elznn0nn  10287  xrleloe  10729  opsrtoslem1  16536  fctop2  17061  alexsubALTlem3  18072  cusgrasizeindslem2  21475  ballotlemfc0  24742  ballotlemfcc  24743  colinearalg  25841  ordcmp  26189  ovoliunnfl  26238  expdioph  27085  en3lpVD  28894  leatb  30027
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