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

Theorem orbi1d 913
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
bid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem orbi1d
StepHypRef Expression
1 bid.1 . . 3 (𝜑 → (𝜓𝜒))
21orbi2d 912 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 866 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 866 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 316 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  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 209  df-or 844
This theorem is referenced by:  orbi1  914  orbi12d  915  eueq2  3700  uneq1  4131  r19.45zv  4447  rexprgf  4630  rextpg  4634  swopolem  5482  ordsseleq  6219  ordtri3  6226  infltoreq  8965  cantnflem1  9151  axgroth2  10246  axgroth3  10252  lelttric  10746  ltxr  12509  xmulneg1  12661  fzpr  12961  elfzp12  12985  caubnd  14717  lcmval  15935  lcmass  15957  isprm6  16057  vdwlem10  16325  irredmul  19458  domneq0  20069  opsrval  20254  znfld  20706  logreclem  25339  perfectlem2  25805  legov3  26383  lnhl  26400  colperpex  26518  lmif  26570  islmib  26572  friendshipgt3  28176  h1datom  29358  xrlelttric  30475  tlt3  30652  prmidl  30957  ismxidl  30971  esumpcvgval  31337  sibfof  31598  satfvsuc  32608  satfv1  32610  satfvsucsuc  32612  satf0suc  32623  sat1el2xp  32626  fmlasuc0  32631  fmlafvel  32632  satfv1fvfmla1  32670  segcon2  33566  poimirlem25  34916  cnambfre  34939  pridl  35314  ismaxidl  35317  ispridlc  35347  pridlc  35348  dmnnzd  35352  4atlem3a  36732  pmapjoin  36987  lcfl3  38629  lcfl4N  38630  sbcoreleleqVD  41193  fourierdlem80  42472  euoreqb  43309  el1fzopredsuc  43526  perfectALTVlem2  43888  nnsum3primesle9  43960  lindslinindsimp2  44519
  Copyright terms: Public domain W3C validator