Theorem orbi12d 931

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860

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 861

This theorem is referenced by:  pm4.39  992  ifpbi123d  1093  3orbi123d  1459  cadbi123d  1633  eueq3  3677  sbcor  3797  unjust  3911  elun  4109  elprg  4608  eltpg  4648  el7g  4652  reuprg0  4664  rabsnifsb  4684  rabrsn  4686  preq12bg  4813  uniprg  4883  disji2  5088  disjprg  5100  disjxun  5102  axprg  5398  swopolem  5569  sotrieq  5590  isso2i  5596  dmopab2rex  5897  somin1  6123  ordequn  6455  fununi  6600  unima  6946  unpreima  7048  eqfunresadj  7348  ordsucun  7809  funcnvuni  7917  fiunlem  7927  frxp  8110  xporderlem  8111  poxp  8112  fnwelem  8115  fnse  8117  xpord2lem  8126  poxp2  8127  xpord3lem  8133  poxp3  8134  soseq  8143  oacan  8521  omword  8543  oeword  8564  oeoa  8571  qsdisj  8780  wemapso2lem  9502  brwdom  9517  cantnflem1  9646  r0weon  9984  infxpen  9986  sornom  10249  fin1ai  10265  isfin5  10271  isfin6  10272  sdom2en01  10274  enfin2i  10293  enfin1ai  10356  isfin5-2  10363  fin1a2lem7  10378  fin1a2lem11  10382  fin1a2lem13  10384  axdc3lem2  10423  engch  10601  eltskg  10723  tsken  10727  ltsonq  10942  addcanpr  11019  ltsosr  11067  axpre-lttri  11138  lemul1  12055  mulge0b  12073  mulle0b  12074  mulsuble0b  12075  nn1m1nn  12242  avgle  12474  nn0sub  12542  elznn0  12594  elz2  12597  nneo  12668  uztric  12874  mul2lt0bi  13112  ltxr  13128  xrrebnd  13182  xmulval  13239  xmulneg1  13283  ixxun  13376  iccsplit  13500  fzsplit2  13565  uzsplit  13612  nelfzo  13681  fzospliti  13708  fzouzsplit  13711  sqeqor  14240  swrdnd  14680  sumeq1  15728  sumeq2w  15731  sumeq2ii  15732  sumeq2sdv  15742  fz1f1o  15749  summo  15756  fsum  15759  prodeq1f  15948  prodeq1  15949  prodeq2w  15952  prodeq2ii  15953  prodeq2sdv  15965  prodmo  15978  fprod  15983  ruclem12  16285  odd2np1lem  16386  dvdsprime  16733  coprm  16758  vdwapun  17022  vdwlem6  17034  vdwlem10  17038  mreexexlemd  17688  mreexexd  17692  istos  18460  tosso  18461  tleile  18463  resstos  18474  tsrlin  18629  tsrss  18633  islring  20613  isdomn  20778  unichnlidl  21328  isprmidl  21422  prmidlc  21432  qsidomlem1  21437  qsidomlem2  21438  prmirredlem  21579  domnchr  21639  zntoslem  21663  znfld  21667  fctop  23118  cctop  23120  ppttop  23121  pptbas  23122  isufil  24017  ufilss  24019  fixufil  24036  fin1aufil  24046  xpsdsval  24495  nlmmul0or  24797  pmltpclem1  25564  iundisj2  25665  mbfmax  25765  dvne0  26127  fta1glem2  26283  plymul0or  26396  ofmulrt  26397  quotval  26410  plydivlem3  26413  plydivlem4  26414  plydivex  26415  plydivalg  26417  quotlem  26418  aalioulem2  26451  quad2  26958  dcubic2  26963  dcubic  26965  dquartlem1  26970  dquart  26972  quart  26980  leibpilem2  27060  wilthlem1  27186  muval2  27252  perfectlem2  27348  lgslem1  27415  pntpbnd1  27704  leslss  28056  abssor  28393  n0s0suc  28489  n0s0m1  28509  nn1m1nns  28521  elzn0s  28545  elzs2  28546  zsoring  28556  n0seo  28568  zseo  28569  bdayfinbndcbv  28613  bdayfinbndlem1  28614  bdayfinbndlem2  28615  bdayfinbnd  28616  z12zsodd  28629  legtrid  28814  legso  28822  ishlg  28825  lnhl  28838  symquadlem  28916  plngcplem  29011  islmib  29035  isinag  29086  isinagd  29087  inaghl  29093  brprlng  29119  brbtwn2  29160  axcontlem2  29220  axcontlem4  29222  axcontlem11  29229  edglnl  29398  nb3grprlem2  29636  hashecclwwlkn1  30333  nfrgr2v  30528  h1datom  31839  atss  32603  atom1d  32610  atord  32645  chirred  32652  elimifd  32795  disji2f  32828  disjif2  32832  disjxpin  32839  iundisj2f  32841  disjunsn  32845  brprop  32950  quad3d  33002  fzsplit3  33046  iundisj2fi  33050  f1ocnt  33053  trleile  33199  domnpropd  33508  subrdom  33513  mxidlmax  33660  rprmval  33718  isrprm  33719  smatrcl  34098  fsumcvg4  34252  erdsze2lem2  35562  satf  35711  satfv1  35721  satfbrsuc  35724  satfrnmapom  35728  satf0op  35735  sat1el2xp  35737  fmlafvel  35743  fmlasuc  35744  fmla1  35745  isfmlasuc  35746  fmlaomn0  35748  fmlasucdisj  35757  satffunlem1lem1  35760  satffunlem1lem2  35761  satffunlem2lem1  35762  dmopab3rexdif  35763  satffunlem2lem2  35764  satfv1fvfmla1  35781  2goelgoanfmla1  35782  satefvfmla1  35783  funpsstri  36124  seglelin  36474  lineunray  36505  prodeq12sdv  36586  cbvsumdavw  36647  cbvproddavw  36648  cbvsumdavw2  36663  cbvproddavw2  36664  weiunval  36830  axtcond  36846  topdifinffinlem  37848  topdifinffin  37849  topdifinfeq  37851  mblfinlem2  38164  itg2addnclem2  38178  iblabsnclem  38189  ftc1anclem5  38203  fdc1  38252  unichnidl  38537  ispridl  38540  maxidlmax  38549  disjressuc2  38917  qsdisjALTV  39205  lcvexchlem4  39668  lcvexchlem5  39669  2at0mat0  40156  pmapjoin  40483  cdlemg17h  41299  dihlspsnat  41964  lzunuz  43356  dvdsrabdioph  43394  acongeq12d  43563  jm2.25  43583  rmydioph  43598  expdioph  43607  fnwe2val  43633  aomclem8  43645  fzunt  44038  fzuntd  44039  fzunt1d  44040  fzuntgd  44041  sqrtcvallem1  44214  brfvrcld2  44275  uneqsn  44608  ntrneixb  44678  ntrneix3  44680  ntrneix13  44682  mnringmulrcld  44811  disjinfi  45769  salexct  46907  salexct2  46912  salexct3  46915  salgencntex  46916  salgensscntex  46917  nnfoctbdjlem  47028  nnfoctbdj  47029  iundjiun  47033  opprb  47624  euoreqb  47702  el1fzopredsuc  47919  iccpartgel  48034  paireqne  48116  divgcdoddALTV  48303  perfectALTVlem2  48343  clnbgrel  48449  dfvopnbgr2  48474  vopnbgrel  48475  dfclnbgr6  48477  dfnbgr6  48478  clnbgrgrim  48555  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem2  48693  gpg5nbgrvtx13starlem3  48694  gpg5edgnedg  48751  lindslinindsimp2lem5  49094  ldepspr  49105  rrx2pnedifcoorneor  49348  rrx2plord  49352  rrx2plordisom  49355  itsclc0yqsol  49396