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

Theorem orbi2i 927
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
Hypothesis
Ref Expression
orbi2i.1 (𝜑𝜓)
Assertion
Ref Expression
orbi2i ((𝜒𝜑) ↔ (𝜒𝜓))

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4 (𝜑𝜓)
21biimpi 207 . . 3 (𝜑𝜓)
32orim2i 925 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 219 . . 3 (𝜓𝜑)
54orim2i 925 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 200 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 865
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 198  df-or 866
This theorem is referenced by:  orbi1i  928  orbi12i  929  orass  936  or4  941  or42  942  orordir  944  dn1  1073  dfifp6  1084  3orcombOLD  1108  excxor  1623  nf3  1866  nfnbi  1940  19.44v  2090  19.44  2273  r19.30  3266  sspsstri  3901  unass  3963  undi  4070  undif3  4084  undif4  4225  ssunpr  4547  sspr  4548  sstp  4549  pr1eqbg  4570  iinun2  4771  iinuni  4794  qfto  5722  somin1  5734  ordtri2  5965  on0eqel  6052  frxp  7515  wfrlem14  7658  wfrlem15  7659  supgtoreq  8609  wemapsolem  8688  fin1a2lem12  9512  psslinpr  10132  suplem2pr  10154  fimaxre  11247  elnn0  11555  elxnn0  11625  elnn1uz2  11978  elxr  12160  xrinfmss  12352  elfzp1  12608  hashf1lem2  13451  dvdslelem  15248  pythagtrip  15750  tosso  17235  maducoeval2  20651  madugsum  20654  ist0-3  21357  limcdif  23848  ellimc2  23849  limcmpt  23855  limcres  23858  plydivex  24260  taylfval  24321  legtrid  25694  legso  25702  lmicom  25888  numedglnl  26248  nb3grprlem2  26493  clwwlkneq0  27170  numclwwlk3lemOLD  27563  atomli  29563  atoml2i  29564  or3di  29629  disjnf  29703  disjex  29724  disjexc  29725  orngsqr  30123  ind1a  30400  esumcvg  30467  voliune  30611  volfiniune  30612  bnj964  31330  dfso2  31960  soseq  32069  lineunray  32569  bj-dfbi4  32866  poimirlem18  33734  poimirlem23  33739  poimirlem27  33743  poimirlem31  33747  itg2addnclem2  33768  tsxo1  34248  tsxo2  34249  tsxo3  34250  tsxo4  34251  tsna1  34255  tsna2  34256  tsna3  34257  ts3an1  34261  ts3an2  34262  ts3an3  34263  ts3or1  34264  ts3or2  34265  ts3or3  34266  ifpim123g  38339  ifpor123g  38347  rp-fakeoranass  38353  frege133d  38551  or3or  38813  undif3VD  39606  wallispilem3  40757  iccpartgt  41932  nnsum4primeseven  42257  nnsum4primesevenALTV  42258  lindslinindsimp2  42814
  Copyright terms: Public domain W3C validator