Theorem orbi12d 917

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

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi1d 915	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		bi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 914	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 846

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 207  df-or 847

This theorem is referenced by:  pm4.39  977  ifpbi123d  1079  3orbi123d  1435  cadbi123d  1607  eueq3  3733  sbcor  3858  unjust  3980  elun  4176  elprg  4670  eltpg  4709  el7g  4713  reuprg0  4727  rabsnifsb  4747  rabrsn  4749  preq12bg  4878  uniprg  4947  disji2  5150  disjprg  5162  disjxun  5164  swopolem  5618  sotrieq  5638  isso2i  5644  dmopab2rex  5942  somin1  6165  ordequn  6498  fununi  6653  unima  6997  unpreima  7096  eqfunresadj  7396  ordsucun  7861  funcnvuni  7972  fiunlem  7982  frxp  8167  xporderlem  8168  poxp  8169  fnwelem  8172  fnse  8174  xpord2lem  8183  poxp2  8184  xpord3lem  8190  poxp3  8191  soseq  8200  oacan  8604  omword  8626  oeword  8646  oeoa  8653  qsdisj  8852  wemapso2lem  9621  brwdom  9636  cantnflem1  9758  r0weon  10081  infxpen  10083  sornom  10346  fin1ai  10362  isfin5  10368  isfin6  10369  sdom2en01  10371  enfin2i  10390  enfin1ai  10453  isfin5-2  10460  fin1a2lem7  10475  fin1a2lem11  10479  fin1a2lem13  10481  axdc3lem2  10520  engch  10697  eltskg  10819  tsken  10823  ltsonq  11038  addcanpr  11115  ltsosr  11163  axpre-lttri  11234  lemul1  12146  mulge0b  12165  mulle0b  12166  mulsuble0b  12167  nn1m1nn  12314  avgle  12535  nn0sub  12603  elznn0  12654  elz2  12657  nneo  12727  uztric  12927  mul2lt0bi  13163  ltxr  13178  xrrebnd  13230  xmulval  13287  xmulneg1  13331  ixxun  13423  iccsplit  13545  fzsplit2  13609  uzsplit  13656  nelfzo  13721  fzospliti  13748  fzouzsplit  13751  sqeqor  14265  swrdnd  14702  sumeq1  15737  sumeq2w  15740  sumeq2ii  15741  sumeq2sdv  15751  fz1f1o  15758  summo  15765  fsum  15768  prodeq1f  15954  prodeq1  15955  prodeq2w  15958  prodeq2ii  15959  prodeq2sdv  15971  prodmo  15984  fprod  15989  ruclem12  16289  odd2np1lem  16388  dvdsprime  16734  coprm  16758  vdwapun  17021  vdwlem6  17033  vdwlem10  17037  mreexexlemd  17702  mreexexd  17706  istos  18488  tosso  18489  tleile  18491  tsrlin  18655  tsrss  18659  islring  20566  isdomn  20727  prmirredlem  21506  domnchr  21570  zntoslem  21598  znfld  21602  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  isufil  23932  ufilss  23934  fixufil  23951  fin1aufil  23961  xpsdsval  24412  nlmmul0or  24725  pmltpclem1  25502  iundisj2  25603  mbfmax  25703  dvne0  26070  fta1glem2  26228  plymul0or  26340  ofmulrt  26341  quotval  26352  plydivlem3  26355  plydivlem4  26356  plydivex  26357  plydivalg  26359  quotlem  26360  aalioulem2  26393  quad2  26900  dcubic2  26905  dcubic  26907  dquartlem1  26912  dquart  26914  quart  26922  leibpilem2  27002  wilthlem1  27129  muval2  27195  perfectlem2  27292  lgslem1  27359  pntpbnd1  27648  slelss  27964  abssor  28288  n0s0suc  28363  n0s0m1  28377  elzn0s  28402  elzs2  28403  n0seo  28423  zseo  28424  legtrid  28617  legso  28625  ishlg  28628  lnhl  28641  symquadlem  28715  islmib  28813  isinag  28864  isinagd  28865  inaghl  28871  brbtwn2  28938  axcontlem2  28998  axcontlem4  29000  axcontlem11  29007  edglnl  29178  nb3grprlem2  29416  hashecclwwlkn1  30109  nfrgr2v  30304  h1datom  31614  atss  32378  atom1d  32385  atord  32420  chirred  32427  elimifd  32566  disji2f  32599  disjif2  32603  disjxpin  32610  iundisj2f  32612  disjunsn  32616  brprop  32709  quad3d  32757  fzsplit3  32799  iundisj2fi  32802  f1ocnt  32807  resstos  32940  trleile  32944  subrdom  33254  isprmidl  33431  prmidlc  33441  qsidomlem1  33445  qsidomlem2  33446  mxidlmax  33458  rprmval  33509  isrprm  33510  smatrcl  33742  fsumcvg4  33896  erdsze2lem2  35172  satf  35321  satfv1  35331  satfbrsuc  35334  satfrnmapom  35338  satf0op  35345  sat1el2xp  35347  fmlafvel  35353  fmlasuc  35354  fmla1  35355  isfmlasuc  35356  fmlaomn0  35358  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem1lem2  35371  satffunlem2lem1  35372  dmopab3rexdif  35373  satffunlem2lem2  35374  satfv1fvfmla1  35391  2goelgoanfmla1  35392  satefvfmla1  35393  funpsstri  35729  seglelin  36080  lineunray  36111  prodeq12sdv  36184  cbvsumdavw  36245  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  weiunlem1  36428  topdifinffinlem  37313  topdifinffin  37314  topdifinfeq  37316  mblfinlem2  37618  itg2addnclem2  37632  iblabsnclem  37643  ftc1anclem5  37657  fdc1  37706  unichnidl  37991  ispridl  37994  maxidlmax  38003  disjressuc2  38344  qsdisjALTV  38571  lcvexchlem4  38993  lcvexchlem5  38994  2at0mat0  39482  pmapjoin  39809  cdlemg17h  40625  dihlspsnat  41290  lzunuz  42724  dvdsrabdioph  42766  acongeq12d  42936  jm2.25  42956  rmydioph  42971  expdioph  42980  fnwe2val  43006  aomclem8  43018  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  sqrtcvallem1  43593  brfvrcld2  43654  uneqsn  43987  ntrneixb  44057  ntrneix3  44059  ntrneix13  44061  mnringmulrcld  44197  disjinfi  45099  salexct  46255  salexct2  46260  salexct3  46263  salgencntex  46264  salgensscntex  46265  nnfoctbdjlem  46376  nnfoctbdj  46377  iundjiun  46381  opprb  46946  euoreqb  47024  el1fzopredsuc  47240  iccpartgel  47303  paireqne  47385  divgcdoddALTV  47556  perfectALTVlem2  47596  clnbgrel  47701  dfvopnbgr2  47725  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  clnbgrgrim  47786  lindslinindsimp2lem5  48191  ldepspr  48202  rrx2pnedifcoorneor  48450  rrx2plord  48454  rrx2plordisom  48457  itsclc0yqsol  48498