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

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

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 389 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 522 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 389 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 275 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  orbi12i  524  orordi  533  3anor  1001  3or6  1350  cadan  1512  19.45v  1829  19.45  2050  unass  3591  tz7.48lem  7158  dffin7-2  8828  zorng  8934  entri2  8983  grothprim  9259  leloe  9720  arch  10866  elznn0nn  10951  xrleloe  11443  ressval3d  15186  opsrtoslem1  18707  fctop2  20020  alexsubALTlem3  21064  colinearalg  24940  cusgrasizeindslem2  25202  disjnf  28181  ballotlemfc0  29325  ballotlemfcc  29326  ordcmp  31107  bj-nfn  31219  poimirlem21  31961  ovoliunnfl  31982  biimpor  32317  tsim1  32372  leatb  32858  expdioph  35878  ifpim123g  36144  ifpimimb  36148  ifpororb  36149  rp-fakeinunass  36160  sbc3or  36889  en3lpVD  37241  el1fzopredsuc  38722  iccpartgt  38741  ldepspr  40319
  Copyright terms: Public domain W3C validator