Theorem orbi12d 918

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 916	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		bi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 915	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

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

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 848

This theorem is referenced by:  pm4.39  978  ifpbi123d  1078  3orbi123d  1437  cadbi123d  1610  eueq3  3682  sbcor  3804  unjust  3918  elun  4116  elprg  4612  eltpg  4650  el7g  4654  reuprg0  4666  rabsnifsb  4686  rabrsn  4688  preq12bg  4817  uniprg  4887  disji2  5091  disjprg  5103  disjxun  5105  swopolem  5556  sotrieq  5577  isso2i  5583  dmopab2rex  5881  somin1  6106  ordequn  6437  fununi  6591  unima  6936  unpreima  7035  eqfunresadj  7335  ordsucun  7800  funcnvuni  7908  fiunlem  7920  frxp  8105  xporderlem  8106  poxp  8107  fnwelem  8110  fnse  8112  xpord2lem  8121  poxp2  8122  xpord3lem  8128  poxp3  8129  soseq  8138  oacan  8512  omword  8534  oeword  8554  oeoa  8561  qsdisj  8767  wemapso2lem  9505  brwdom  9520  cantnflem1  9642  r0weon  9965  infxpen  9967  sornom  10230  fin1ai  10246  isfin5  10252  isfin6  10253  sdom2en01  10255  enfin2i  10274  enfin1ai  10337  isfin5-2  10344  fin1a2lem7  10359  fin1a2lem11  10363  fin1a2lem13  10365  axdc3lem2  10404  engch  10581  eltskg  10703  tsken  10707  ltsonq  10922  addcanpr  10999  ltsosr  11047  axpre-lttri  11118  lemul1  12034  mulge0b  12053  mulle0b  12054  mulsuble0b  12055  nn1m1nn  12207  avgle  12424  nn0sub  12492  elznn0  12544  elz2  12547  nneo  12618  uztric  12817  mul2lt0bi  13059  ltxr  13075  xrrebnd  13128  xmulval  13185  xmulneg1  13229  ixxun  13322  iccsplit  13446  fzsplit2  13510  uzsplit  13557  nelfzo  13625  fzospliti  13652  fzouzsplit  13655  sqeqor  14181  swrdnd  14619  sumeq1  15655  sumeq2w  15658  sumeq2ii  15659  sumeq2sdv  15669  fz1f1o  15676  summo  15683  fsum  15686  prodeq1f  15872  prodeq1  15873  prodeq2w  15876  prodeq2ii  15877  prodeq2sdv  15889  prodmo  15902  fprod  15907  ruclem12  16209  odd2np1lem  16310  dvdsprime  16657  coprm  16681  vdwapun  16945  vdwlem6  16957  vdwlem10  16961  mreexexlemd  17605  mreexexd  17609  istos  18377  tosso  18378  tleile  18380  tsrlin  18544  tsrss  18548  islring  20449  isdomn  20614  prmirredlem  21382  domnchr  21442  zntoslem  21466  znfld  21470  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  isufil  23790  ufilss  23792  fixufil  23809  fin1aufil  23819  xpsdsval  24269  nlmmul0or  24571  pmltpclem1  25349  iundisj2  25450  mbfmax  25550  dvne0  25916  fta1glem2  26074  plymul0or  26188  ofmulrt  26189  quotval  26200  plydivlem3  26203  plydivlem4  26204  plydivex  26205  plydivalg  26207  quotlem  26208  aalioulem2  26241  quad2  26749  dcubic2  26754  dcubic  26756  dquartlem1  26761  dquart  26763  quart  26771  leibpilem2  26851  wilthlem1  26978  muval2  27044  perfectlem2  27141  lgslem1  27208  pntpbnd1  27497  slelss  27820  abssor  28148  n0s0suc  28234  n0s0m1  28252  nn1m1nns  28263  elzn0s  28286  elzs2  28287  n0seo  28307  zseo  28308  legtrid  28518  legso  28526  ishlg  28529  lnhl  28542  symquadlem  28616  islmib  28714  isinag  28765  isinagd  28766  inaghl  28772  brbtwn2  28832  axcontlem2  28892  axcontlem4  28894  axcontlem11  28901  edglnl  29070  nb3grprlem2  29308  hashecclwwlkn1  30006  nfrgr2v  30201  h1datom  31511  atss  32275  atom1d  32282  atord  32317  chirred  32324  elimifd  32472  disji2f  32506  disjif2  32510  disjxpin  32517  iundisj2f  32519  disjunsn  32523  brprop  32620  quad3d  32673  fzsplit3  32716  iundisj2fi  32720  f1ocnt  32725  resstos  32893  trleile  32897  domnpropd  33227  subrdom  33235  isprmidl  33409  prmidlc  33419  qsidomlem1  33423  qsidomlem2  33424  mxidlmax  33436  rprmval  33487  isrprm  33488  smatrcl  33786  fsumcvg4  33940  erdsze2lem2  35191  satf  35340  satfv1  35350  satfbrsuc  35353  satfrnmapom  35357  satf0op  35364  sat1el2xp  35366  fmlafvel  35372  fmlasuc  35373  fmla1  35374  isfmlasuc  35375  fmlaomn0  35377  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem1lem2  35390  satffunlem2lem1  35391  dmopab3rexdif  35392  satffunlem2lem2  35393  satfv1fvfmla1  35410  2goelgoanfmla1  35411  satefvfmla1  35412  funpsstri  35753  seglelin  36104  lineunray  36135  prodeq12sdv  36206  cbvsumdavw  36267  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  weiunlem1  36450  topdifinffinlem  37335  topdifinffin  37336  topdifinfeq  37338  mblfinlem2  37652  itg2addnclem2  37666  iblabsnclem  37677  ftc1anclem5  37691  fdc1  37740  unichnidl  38025  ispridl  38028  maxidlmax  38037  disjressuc2  38374  qsdisjALTV  38606  lcvexchlem4  39030  lcvexchlem5  39031  2at0mat0  39519  pmapjoin  39846  cdlemg17h  40662  dihlspsnat  41327  lzunuz  42756  dvdsrabdioph  42798  acongeq12d  42968  jm2.25  42988  rmydioph  43003  expdioph  43012  fnwe2val  43038  aomclem8  43050  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  sqrtcvallem1  43620  brfvrcld2  43681  uneqsn  44014  ntrneixb  44084  ntrneix3  44086  ntrneix13  44088  mnringmulrcld  44217  disjinfi  45186  salexct  46332  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  nnfoctbdjlem  46453  nnfoctbdj  46454  iundjiun  46458  opprb  47032  euoreqb  47110  el1fzopredsuc  47326  iccpartgel  47430  paireqne  47512  divgcdoddALTV  47683  perfectALTVlem2  47723  clnbgrel  47829  dfvopnbgr2  47853  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  clnbgrgrim  47934  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  lindslinindsimp2lem5  48451  ldepspr  48462  rrx2pnedifcoorneor  48705  rrx2plord  48709  rrx2plordisom  48712  itsclc0yqsol  48753