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 285 1 ((𝜑𝜒) ↔ (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ 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 196  df-or 384 This theorem is referenced by:  orbi12i  542  orordi  551  3anor  1047  3or6  1402  cadan  1539  19.45v  1900  19.45  2094  unass  3732  tz7.48lem  7423  dffin7-2  9103  zorng  9209  entri2  9259  grothprim  9535  leloe  10003  arch  11166  elznn0nn  11268  xrleloe  11853  ressval3d  15764  opsrtoslem1  19305  fctop2  20619  alexsubALTlem3  21663  colinearalg  25590  cusgrasizeindslem1  26002  disjnf  28766  ballotlemfc0  29881  ballotlemfcc  29882  ordcmp  31616  bj-nfn  31795  poimirlem21  32600  ovoliunnfl  32621  biimpor  33053  tsim1  33107  leatb  33597  expdioph  36608  ifpim123g  36864  ifpimimb  36868  ifpororb  36869  rp-fakeinunass  36880  andi3or  37340  uneqsn  37341  sbc3or  37759  en3lpVD  38102  el1fzopredsuc  39948  iccpartgt  39965  fmtno4prmfac  40022  ldepspr  42056
 Copyright terms: Public domain W3C validator