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

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

Proof of Theorem orbi2d
StepHypRef Expression
1 bid.1 . . 3 (𝜑 → (𝜓𝜒))
21imbi2d 342 . 2 (𝜑 → ((¬ 𝜃𝜓) ↔ (¬ 𝜃𝜒)))
3 df-or 842 . 2 ((𝜃𝜓) ↔ (¬ 𝜃𝜓))
4 df-or 842 . 2 ((𝜃𝜒) ↔ (¬ 𝜃𝜒))
52, 3, 43bitr4g 315 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wo 841
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 208  df-or 842
This theorem is referenced by:  orbi1d  910  orbi12d  912  eueq2  3698  sbc2or  3778  r19.44zv  4445  rexprgf  4623  rextpg  4627  swopolem  5476  poleloe  5984  elsucg  6251  elsuc2g  6252  brdifun  8307  brwdom  9019  isfin1a  9702  elgch  10032  suplem2pr  10463  axlttri  10700  mulcan1g  11281  elznn0  11984  elznn  11985  zindd  12071  rpneg  12409  dfle2  12528  fzm1  12975  fzosplitsni  13136  hashv01gt1  13693  zeo5  15693  bitsf1  15783  lcmval  15924  lcmneg  15935  lcmass  15946  isprm6  16046  infpn2  16237  irredmul  19388  domneq0  19998  znfld  20635  quotval  24808  plydivlem4  24812  plydivex  24813  aalioulem2  24849  aalioulem5  24852  aalioulem6  24853  aaliou  24854  aaliou2  24856  aaliou2b  24857  isinag  26551  axcontlem7  26683  hashecclwwlkn1  27783  elunsn  30200  eliccioo  30534  tlt2  30578  prmidl  30876  sibfof  31497  ballotlemfc0  31649  ballotlemfcc  31650  satfvsucsuc  32509  satf0op  32521  fmlafvel  32529  isfmlasuc  32532  satfv1fvfmla1  32567  seglelin  33474  lineunray  33505  topdifinfeq  34513  mblfinlem2  34811  pridl  35196  maxidlval  35198  ispridlc  35229  pridlc  35230  dmnnzd  35234  lcfl7N  38517  aomclem8  39539  orbi1r  40721  iccpartgtl  43463  iccpartleu  43465  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  rrx2pnedifcoorneorr  44632
  Copyright terms: Public domain W3C validator