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

Theorem orbi2i 541
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 206 . . 3 (𝜑𝜓)
32orim2i 540 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 218 . . 3 (𝜓𝜑)
54orim2i 540 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 199 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383
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 197  df-or 385
This theorem is referenced by:  orbi1i  542  orbi12i  543  orass  546  or4  550  or42  551  orordir  553  dn1  1007  dfifp6  1017  3orcomb  1046  excxor  1466  nf3  1709  19.44v  1909  19.44  2104  r19.30  3075  sspsstri  3692  unass  3753  undi  3855  undif3  3869  undif3OLD  3870  undif4  4012  ssunpr  4338  sspr  4339  sstp  4340  pr1eqbg  4363  iinun2  4557  iinuni  4580  qfto  5481  somin1  5493  ordtri2  5722  on0eqel  5809  frxp  7239  wfrlem14  7380  wfrlem15  7381  supgtoreq  8328  wemapsolem  8407  fin1a2lem12  9185  psslinpr  9805  suplem2pr  9827  fimaxre  10920  elnn0  11246  elxnn0  11317  elnn1uz2  11717  elxr  11902  xrinfmss  12091  elfzp1  12341  hashf1lem2  13186  dvdslelem  14966  pythagtrip  15474  tosso  16968  maducoeval2  20378  madugsum  20381  ist0-3  21072  limcdif  23563  ellimc2  23564  limcmpt  23570  limcres  23573  plydivex  23973  taylfval  24034  legtrid  25403  legso  25411  lmicom  25597  nb3grprlem2  26187  numclwwlk3lem  27113  atomli  29111  atoml2i  29112  or3di  29177  disjnf  29252  disjex  29273  disjexc  29274  orngsqr  29613  ind1a  29888  esumcvg  29953  voliune  30097  volfiniune  30098  bnj964  30756  dfso2  31387  socnv  31398  soseq  31487  lineunray  31931  bj-dfbi4  32235  poimirlem18  33094  poimirlem23  33099  poimirlem27  33103  poimirlem31  33107  itg2addnclem2  33129  tsxo1  33611  tsxo2  33612  tsxo3  33613  tsxo4  33614  tsna1  33618  tsna2  33619  tsna3  33620  ts3an1  33624  ts3an2  33625  ts3an3  33626  ts3or1  33627  ts3or2  33628  ts3or3  33629  ifpim123g  37361  ifpor123g  37369  rp-fakeoranass  37375  frege133d  37573  or3or  37836  undif3VD  38636  wallispilem3  39617  iccpartgt  40687  nnsum4primeseven  41003  nnsum4primesevenALTV  41004  lindslinindsimp2  41566
  Copyright terms: Public domain W3C validator