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

Theorem orbi12d 742
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
bi12d.1 (𝜑 → (𝜓𝜒))
bi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
orbi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem orbi12d
StepHypRef Expression
1 bi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21orbi1d 735 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 734 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 267 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  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:  pm4.39  911  ifpbi123d  1021  3orbi123d  1390  cadbi123d  1540  eueq3  3348  sbcor  3446  unjust  3544  elun  3715  elprg  4144  eltpg  4174  rabsnifsb  4201  rabrsn  4203  preq12bg  4326  disji2  4569  disjprg  4578  disjxun  4581  swopolem  4968  sotrieq  4986  isso2i  4991  somin1  5448  ordequn  5745  fununi  5878  unpreima  6249  ordsucun  6917  funcnvuni  7012  fun11iun  7019  frxp  7174  xporderlem  7175  poxp  7176  fnwelem  7179  fnse  7181  oacan  7515  omword  7537  oeword  7557  oeoa  7564  qsdisj  7711  wemapso2lem  8340  brwdom  8355  cantnflem1  8469  r0weon  8718  infxpen  8720  sornom  8982  fin1ai  8998  isfin5  9004  isfin6  9005  sdom2en01  9007  enfin2i  9026  enfin1ai  9089  isfin5-2  9096  fin1a2lem7  9111  fin1a2lem11  9115  fin1a2lem13  9117  axdc3lem2  9156  engch  9329  eltskg  9451  tsken  9455  ltsonq  9670  addcanpr  9747  ltsosr  9794  axpre-lttri  9865  lemul1  10754  mulge0b  10772  mulle0b  10773  mulsuble0b  10774  nn1m1nn  10917  avgle  11151  nn0sub  11220  elznn0  11269  elz2  11271  nneo  11337  uztric  11585  mul2lt0bi  11812  ltxr  11825  xrrebnd  11873  xmulval  11930  xmulneg1  11971  ixxun  12062  iccsplit  12176  fzsplit2  12237  uzsplit  12281  nelfzo  12344  fzospliti  12369  fzouzsplit  12372  sqeqor  12840  swrdnd  13284  sumeq1  14267  sumeq2w  14270  sumeq2ii  14271  fz1f1o  14288  summo  14295  fsum  14298  prodeq1f  14477  prodeq2w  14481  prodeq2ii  14482  prodmo  14505  fprod  14510  ruclem12  14809  odd2np1lem  14902  dvdsprime  15238  coprm  15261  vdwapun  15516  vdwlem6  15528  vdwlem10  15532  mreexexlemd  16127  mreexexd  16131  mreexexdOLD  16132  istos  16858  tosso  16859  tsrlin  17042  tsrss  17046  isdomn  19115  prmirredlem  19660  domnchr  19699  zntoslem  19724  znfld  19728  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  isufil  21517  ufilss  21519  fixufil  21536  fin1aufil  21546  xpsdsval  21996  nlmmul0or  22297  pmltpclem1  23024  iundisj2  23124  mbfmax  23222  dvne0  23578  fta1glem2  23730  plymul0or  23840  ofmulrt  23841  quotval  23851  plydivlem3  23854  plydivlem4  23855  plydivex  23856  plydivalg  23858  quotlem  23859  aalioulem2  23892  quad2  24366  dcubic2  24371  dcubic  24373  dquartlem1  24378  dquart  24380  quart  24388  leibpilem2  24468  wilthlem1  24594  muval2  24660  perfectlem2  24755  lgslem1  24822  pntpbnd1  25075  legtrid  25286  legso  25294  ishlg  25297  lnhl  25310  symquadlem  25384  islmib  25479  isinag  25529  inaghl  25531  brbtwn2  25585  axcontlem2  25645  axcontlem4  25647  axcontlem11  25654  nb3graprlem2  25981  hashecclwwlkn1  26361  frgra2v  26526  h1datom  27825  atss  28589  atom1d  28596  atord  28631  chirred  28638  elimifd  28746  disji2f  28772  disjif2  28776  disjxpin  28783  iundisj2f  28785  disjunsn  28789  fzsplit3  28940  iundisj2fi  28943  f1ocnt  28946  resstos  28991  tleile  28992  trleile  28997  smatrcl  29190  fsumcvg4  29324  erdsze2lem2  30440  funpsstri  30909  soseq  30995  seglelin  31393  lineunray  31424  topdifinffinlem  32371  topdifinffin  32372  topdifinfeq  32374  mblfinlem2  32617  itg2addnclem2  32632  iblabsnclem  32643  ftc1anclem5  32659  fdc1  32712  unichnidl  33000  ispridl  33003  maxidlmax  33012  lcvexchlem4  33342  lcvexchlem5  33343  2at0mat0  33829  pmapjoin  34156  cdlemg17h  34974  dihlspsnat  35640  lzunuz  36349  dvdsrabdioph  36392  acongeq12d  36564  jm2.25  36584  rmydioph  36599  expdioph  36608  fnwe2val  36637  aomclem8  36649  brfvrcld2  37003  uneqsn  37341  ntrneixb  37413  ntrneix3  37415  ntrneix13  37417  sbcorgOLD  37761  unima  38340  disjinfi  38375  salexct  39228  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  nnfoctbdjlem  39348  nnfoctbdj  39349  iundjiun  39353  el1fzopredsuc  39948  iccpartgel  39967  divgcdoddALTV  40131  perfectALTVlem2  40165  nb3grprlem2  40609  hashecclwwlksn1  41261  nfrgr2v  41442  lindslinindsimp2lem5  42045  ldepspr  42056
  Copyright terms: Public domain W3C validator