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

Theorem orbi12d 916
 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 914 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 913 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 282 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  pm4.39  974  ifpbi123d  1075  ifpbi123dOLD  1076  3orbi123d  1432  cadbi123d  1612  eueq3  3650  sbcor  3769  unjust  3885  elun  4076  elprg  4546  eltpg  4583  reuprg0  4598  rabsnifsb  4618  rabrsn  4620  preq12bg  4744  disji2  5013  disjprgw  5026  disjprg  5027  disjxun  5029  swopolem  5448  sotrieq  5467  isso2i  5473  dmopab2rex  5751  somin1  5961  ordequn  6260  fununi  6400  unima  6715  unpreima  6811  ordsucun  7523  funcnvuni  7621  fiunlem  7628  frxp  7806  xporderlem  7807  poxp  7808  fnwelem  7811  fnse  7813  oacan  8160  omword  8182  oeword  8202  oeoa  8209  qsdisj  8360  wemapso2lem  9003  brwdom  9018  cantnflem1  9139  r0weon  9426  infxpen  9428  sornom  9691  fin1ai  9707  isfin5  9713  isfin6  9714  sdom2en01  9716  enfin2i  9735  enfin1ai  9798  isfin5-2  9805  fin1a2lem7  9820  fin1a2lem11  9824  fin1a2lem13  9826  axdc3lem2  9865  engch  10042  eltskg  10164  tsken  10168  ltsonq  10383  addcanpr  10460  ltsosr  10508  axpre-lttri  10579  lemul1  11484  mulge0b  11502  mulle0b  11503  mulsuble0b  11504  nn1m1nn  11649  avgle  11870  nn0sub  11938  elznn0  11987  elz2  11990  nneo  12057  uztric  12257  mul2lt0bi  12486  ltxr  12501  xrrebnd  12552  xmulval  12609  xmulneg1  12653  ixxun  12745  iccsplit  12866  fzsplit2  12930  uzsplit  12977  nelfzo  13041  fzospliti  13067  fzouzsplit  13070  sqeqor  13577  swrdnd  14010  sumeq1  15040  sumeq2w  15044  sumeq2ii  15045  fz1f1o  15062  summo  15069  fsum  15072  prodeq1f  15257  prodeq2w  15261  prodeq2ii  15262  prodmo  15285  fprod  15290  ruclem12  15589  odd2np1lem  15684  dvdsprime  16024  coprm  16048  vdwapun  16303  vdwlem6  16315  vdwlem10  16319  mreexexlemd  16910  mreexexd  16914  istos  17640  tosso  17641  tsrlin  17824  tsrss  17828  isdomn  20064  prmirredlem  20191  domnchr  20229  zntoslem  20253  znfld  20257  fctop  21619  cctop  21621  ppttop  21622  pptbas  21623  isufil  22518  ufilss  22520  fixufil  22537  fin1aufil  22547  xpsdsval  22998  nlmmul0or  23299  pmltpclem1  24062  iundisj2  24163  mbfmax  24263  dvne0  24624  fta1glem2  24777  plymul0or  24887  ofmulrt  24888  quotval  24898  plydivlem3  24901  plydivlem4  24902  plydivex  24903  plydivalg  24905  quotlem  24906  aalioulem2  24939  quad2  25435  dcubic2  25440  dcubic  25442  dquartlem1  25447  dquart  25449  quart  25457  leibpilem2  25537  wilthlem1  25663  muval2  25729  perfectlem2  25824  lgslem1  25891  pntpbnd1  26180  legtrid  26395  legso  26403  ishlg  26406  lnhl  26419  symquadlem  26493  islmib  26591  isinag  26642  isinagd  26643  inaghl  26649  brbtwn2  26709  axcontlem2  26769  axcontlem4  26771  axcontlem11  26778  edglnl  26946  nb3grprlem2  27181  hashecclwwlkn1  27872  nfrgr2v  28067  h1datom  29375  atss  30139  atom1d  30146  atord  30181  chirred  30188  elimifd  30320  disji2f  30350  disjif2  30354  disjxpin  30361  iundisj2f  30363  disjunsn  30367  brprop  30467  fzsplit3  30553  iundisj2fi  30556  f1ocnt  30561  resstos  30683  tleile  30684  trleile  30689  isprmidl  31031  prmidlc  31042  qsidomlem1  31046  qsidomlem2  31047  mxidlmax  31055  rprmval  31082  isrprm  31083  smatrcl  31164  fsumcvg4  31318  erdsze2lem2  32579  satf  32728  satfv1  32738  satfbrsuc  32741  satfrnmapom  32745  satf0op  32752  sat1el2xp  32754  fmlafvel  32760  fmlasuc  32761  fmla1  32762  isfmlasuc  32763  fmlaomn0  32765  fmlasucdisj  32774  satffunlem1lem1  32777  satffunlem1lem2  32778  satffunlem2lem1  32779  dmopab3rexdif  32780  satffunlem2lem2  32781  satfv1fvfmla1  32798  2goelgoanfmla1  32799  satefvfmla1  32800  eqfunresadj  33132  funpsstri  33136  soseq  33224  seglelin  33705  lineunray  33736  topdifinffinlem  34783  topdifinffin  34784  topdifinfeq  34786  mblfinlem2  35114  itg2addnclem2  35128  iblabsnclem  35139  ftc1anclem5  35153  fdc1  35203  unichnidl  35488  ispridl  35491  maxidlmax  35500  qsdisjALTV  36029  lcvexchlem4  36352  lcvexchlem5  36353  2at0mat0  36840  pmapjoin  37167  cdlemg17h  37983  dihlspsnat  38648  lzunuz  39752  dvdsrabdioph  39794  acongeq12d  39963  jm2.25  39983  rmydioph  39998  expdioph  40007  fnwe2val  40036  aomclem8  40048  sqrtcvallem1  40374  brfvrcld2  40436  uneqsn  40769  ntrneixb  40841  ntrneix3  40843  ntrneix13  40845  mnringmulrcld  40979  disjinfi  41863  salexct  43017  salexct2  43022  salexct3  43025  salgencntex  43026  salgensscntex  43027  nnfoctbdjlem  43137  nnfoctbdj  43138  iundjiun  43142  opprb  43666  euoreqb  43708  el1fzopredsuc  43925  iccpartgel  43989  paireqne  44071  divgcdoddALTV  44243  perfectALTVlem2  44283  lindslinindsimp2lem5  44912  ldepspr  44923  rrx2pnedifcoorneor  45171  rrx2plord  45175  rrx2plordisom  45178  itsclc0yqsol  45219
 Copyright terms: Public domain W3C validator