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

Theorem orbi1i 937
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 896 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 936 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 896 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 288 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 873
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 874
This theorem is referenced by:  orbi12i  938  orordi  952  3anorOLD  1130  3ianor  1132  3or6  1571  cadan  1718  nfnbiOLD  1951  19.45v  2093  19.45  2272  unass  3931  tz7.48lem  7739  dffin7-2  9472  zorng  9578  entri2  9632  grothprim  9908  leloe  10377  arch  11534  elznn0nn  11637  xrleloe  12176  ressval3d  16210  ressval3dOLD  16211  opsrtoslem1  19756  fctop2  21088  alexsubALTlem3  22131  colinearalg  26080  numclwwlk3lem2  27634  disjnf  29766  ballotlemfc0  30936  ballotlemfcc  30937  noextenddif  32196  sleloe  32254  ordcmp  32816  poimirlem21  33786  ovoliunnfl  33807  biimpor  34237  tsim1  34290  leatb  35180  expdioph  38199  ifpim123g  38453  ifpimimb  38457  ifpororb  38458  rp-fakeinunass  38468  andi3or  38926  uneqsn  38927  sbc3or  39342  en3lpVD  39665  el1fzopredsuc  42001  iccpartgt  42029  fmtno4prmfac  42092  ldepspr  42863
  Copyright terms: Public domain W3C validator