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

Theorem orbi2i 910
 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 219 . . 3 (𝜑𝜓)
32orim2i 908 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 231 . . 3 (𝜓𝜑)
54orim2i 908 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 212 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  orbi1i  911  orbi12i  912  orass  919  or4  924  or42  925  orordir  927  dn1  1053  dfifp6  1064  excxor  1508  nf3  1788  nfnbi  1856  19.44v  1999  19.44  2238  sspsstri  4033  unass  4096  undi  4204  undif3  4218  2nreu  4352  undif4  4377  ssunpr  4728  sspr  4729  sstp  4730  pr1eqbg  4750  iinun2  4961  iinuni  4986  qfto  5952  somin1  5964  ordtri2  6198  on0eqel  6280  frxp  7807  wfrlem14  7955  wfrlem15  7956  supgtoreq  8922  wemapsolem  9002  fin1a2lem12  9826  psslinpr  10446  suplem2pr  10468  fimaxre  11577  elnn0  11891  elxnn0  11961  elnn1uz2  12317  elxr  12503  xrinfmss  12695  elfzp1  12956  hashf1lem2  13814  dvdslelem  15655  pythagtrip  16165  tosso  17642  maducoeval2  21249  madugsum  21252  ist0-3  21954  limcdif  24483  ellimc2  24484  limcmpt  24490  limcres  24493  plydivex  24897  taylfval  24958  legtrid  26389  legso  26397  lmicom  26586  numedglnl  26941  nb3grprlem2  27175  clwwlkneq0  27818  atomli  30169  atoml2i  30170  or3di  30235  disjnf  30337  disjex  30359  disjexc  30360  cycpmrn  30839  orngsqr  30932  ind1a  31392  esumcvg  31459  voliune  31602  volfiniune  31603  bnj964  32329  satfvsucsuc  32726  satfrnmapom  32731  satf0op  32738  fmlaomn0  32751  dfso2  33104  soseq  33210  frrlem12  33248  lineunray  33722  bj-dfbi4  34020  wl-ifpimpr  34882  wl-df4-3mintru2  34903  poimirlem18  35074  poimirlem23  35079  poimirlem27  35083  poimirlem31  35087  itg2addnclem2  35108  tsxo1  35574  tsxo2  35575  tsxo3  35576  tsxo4  35577  tsna1  35581  tsna2  35582  tsna3  35583  ts3an1  35587  ts3an2  35588  ts3an3  35589  ts3or1  35590  ts3or2  35591  ts3or3  35592  dfeldisj5  36113  ifpim123g  40201  ifpor123g  40209  rp-fakeoranass  40215  ontric3g  40223  frege133d  40459  or3or  40717  undif3VD  41581  wallispilem3  42702  iccpartgt  43937  nnsum4primeseven  44311  nnsum4primesevenALTV  44312  lindslinindsimp2  44865
 Copyright terms: Public domain W3C validator