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

Theorem orbi1i 542
 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 402 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 541 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 402 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 286 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:  orbi12i  543  orordi  552  3anor  1052  3or6  1407  cadan  1545  nfnbi  1778  19.45v  1910  19.45  2105  unass  3754  tz7.48lem  7496  dffin7-2  9180  zorng  9286  entri2  9340  grothprim  9616  leloe  10084  arch  11249  elznn0nn  11351  xrleloe  11937  ressval3d  15877  opsrtoslem1  19424  fctop2  20749  alexsubALTlem3  21793  colinearalg  25724  disjnf  29270  ballotlemfc0  30377  ballotlemfcc  30378  noextenddif  31578  ordcmp  32141  poimirlem21  33101  ovoliunnfl  33122  biimpor  33554  tsim1  33608  leatb  34098  expdioph  37109  ifpim123g  37365  ifpimimb  37369  ifpororb  37370  rp-fakeinunass  37381  andi3or  37841  uneqsn  37842  sbc3or  38259  en3lpVD  38602  el1fzopredsuc  40662  iccpartgt  40691  fmtno4prmfac  40813  ldepspr  41580
 Copyright terms: Public domain W3C validator