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

Theorem orbi1i 910
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 866 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 909 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 866 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 296 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 843
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 206  df-or 844
This theorem is referenced by:  orbi12i  911  orordi  925  3ianor  1105  3or6  1445  norasslem1  1532  norass  1535  cadan  1612  19.45v  1998  19.45  2234  unass  4096  tz7.48lem  8242  dffin7-2  10085  zorng  10191  entri2  10245  grothprim  10521  leloe  10992  arch  12160  elznn0nn  12263  xrleloe  12807  swrdnnn0nd  14297  ressval3d  16882  ressval3dOLD  16883  opsrtoslem1  21172  fctop2  22063  alexsubALTlem3  23108  colinearalg  27181  numclwwlk3lem2  28649  disjnf  30810  ballotlemfc0  32359  ballotlemfcc  32360  satfvsucsuc  33227  satfbrsuc  33228  fmlasuc  33248  otthne  33585  noextenddif  33798  sleloe  33884  ordcmp  34563  wl-df2-3mintru2  35583  poimirlem21  35725  ovoliunnfl  35746  biimpor  36169  tsim1  36215  leatb  37233  metakunt1  40053  expdioph  40761  ifpim123g  41005  ifpimimb  41009  ifpororb  41010  rp-fakeinunass  41020  andi3or  41521  uneqsn  41522  sbc3or  42041  en3lpVD  42354  el1fzopredsuc  44705  iccpartgt  44767  fmtno4prmfac  44912  ldepspr  45702
  Copyright terms: Public domain W3C validator