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

Theorem orbi1i 518
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 385 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 517 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 385 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 271 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 366
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 368
This theorem is referenced by:  orbi12i  519  orordi  528  3anor  987  3or6  1308  cadan  1462  19.45  1975  unass  3647  tz7.48lem  7098  dffin7-2  8769  zorng  8875  entri2  8924  grothprim  9201  leloe  9660  arch  10788  elznn0nn  10874  xrleloe  11353  ressval3d  14783  opsrtoslem1  18346  fctop2  19676  alexsubALTlem3  20718  colinearalg  24418  cusgrasizeindslem2  24679  disjnf  27646  ballotlemfc0  28698  ballotlemfcc  28699  ordcmp  30143  ovoliunnfl  30299  biimpor  30724  tsim1  30780  expdioph  31207  ldepspr  33347  sbc3or  33708  en3lpVD  34064  bj-nfn  34639  leatb  35433  ifpim123g  38122  ifpimimb  38135  ifpororb  38152  rp-fakeinunass  38173
  Copyright terms: Public domain W3C validator