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

Theorem orbi1i 541
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 401 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 540 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 401 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 286 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382
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 384
This theorem is referenced by:  orbi12i  542  orordi  551  3anorOLD  1072  3ianor  1074  3or6  1450  cadan  1588  nfnbi  1821  19.45v  1969  19.45  2145  unass  3803  tz7.48lem  7581  dffin7-2  9258  zorng  9364  entri2  9418  grothprim  9694  leloe  10162  arch  11327  elznn0nn  11429  xrleloe  12015  ressval3d  15984  opsrtoslem1  19532  fctop2  20857  alexsubALTlem3  21900  colinearalg  25835  numclwwlk3lem  27371  disjnf  29510  ballotlemfc0  30682  ballotlemfcc  30683  noextenddif  31946  sleloe  32004  ordcmp  32571  poimirlem21  33560  ovoliunnfl  33581  biimpor  34013  tsim1  34067  leatb  34897  expdioph  37907  ifpim123g  38162  ifpimimb  38166  ifpororb  38167  rp-fakeinunass  38178  andi3or  38637  uneqsn  38638  sbc3or  39055  en3lpVD  39394  el1fzopredsuc  41660  iccpartgt  41688  fmtno4prmfac  41809  ldepspr  42587
  Copyright terms: Public domain W3C validator