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

Theorem orbi2d 734
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 329 . 2 (𝜑 → ((¬ 𝜃𝜓) ↔ (¬ 𝜃𝜒)))
3 df-or 384 . 2 ((𝜃𝜓) ↔ (¬ 𝜃𝜓))
4 df-or 384 . 2 ((𝜃𝜒) ↔ (¬ 𝜃𝜒))
52, 3, 43bitr4g 302 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  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:  orbi1d  735  orbi12d  742  eueq2  3347  sbc2or  3411  r19.44zv  4021  rexprg  4182  rextpg  4184  swopolem  4968  poleloe  5446  elsucg  5709  elsuc2g  5710  brdifun  7658  brwdom  8355  isfin1a  8997  elgch  9323  suplem2pr  9754  axlttri  9988  mulcan1g  10559  elznn0  11269  elznn  11270  zindd  11354  rpneg  11739  dfle2  11856  fzm1  12289  fzosplitsni  12444  hashv01gt1  12995  zeo5  14918  bitsf1  15006  lcmval  15143  lcmneg  15154  lcmass  15165  isprm6  15264  infpn2  15455  irredmul  18532  domneq0  19118  znfld  19728  quotval  23851  plydivlem4  23855  plydivex  23856  aalioulem2  23892  aalioulem5  23895  aalioulem6  23896  aaliou  23897  aaliou2  23899  aaliou2b  23900  isinag  25529  axcontlem7  25650  hashecclwwlkn1  26361  eliccioo  28970  tlt2  28995  sibfof  29729  ballotlemfc0  29881  ballotlemfcc  29882  seglelin  31393  lineunray  31424  topdifinfeq  32374  mblfinlem2  32617  pridl  33006  maxidlval  33008  ispridlc  33039  pridlc  33040  dmnnzd  33044  lcfl7N  35808  aomclem8  36649  orbi1r  37737  iccpartgtl  39964  iccpartleu  39966  hashecclwwlksn1  41261  lindslinindsimp2lem5  42045  lindslinindsimp2  42046
  Copyright terms: Public domain W3C validator