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

Theorem orbi1i 520
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypothesis
Ref Expression
orbi2i.1
Assertion
Ref Expression
orbi1i

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 387 . 2
2 orbi2i.1 . . 3
32orbi2i 519 . 2
4 orcom 387 . 2
51, 3, 43bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368
This theorem is referenced by:  orbi12i  521  orordi  530  3anor  989  3or6  1310  cadan  1459  19.45  1970  unass  3660  tz7.48lem  7125  dffin7-2  8799  zorng  8905  entri2  8954  grothprim  9233  leloe  9692  arch  10817  elznn0nn  10903  xrleloe  11379  opsrtoslem1  18148  fctop2  19506  alexsubALTlem3  20549  colinearalg  24213  cusgrasizeindslem2  24474  disjnf  27433  ballotlemfc0  28431  ballotlemfcc  28432  ordcmp  29912  ovoliunnfl  30056  biimpor  30481  tsim1  30537  expdioph  30965  ressval3d  32558  ldepspr  33074  sbc3or  33302  en3lpVD  33645  bj-nfn  34219  leatb  35017  bj-ifim123g  37706  bj-ifimimb  37715  bj-ifororb  37726  rp-fakeinunass  37740
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
  Copyright terms: Public domain W3C validator