Theorem orbi12d 932

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.39  992  ifpbi123d  1095  3orbi123d  1464  cadbi123d  1643  eueq3  3672  sbcor  3792  unjust  4153  elun  4155  elprg  4607  eltpg  4648  el7g  4652  reuprg0  4664  rabsnifsb  4685  rabrsn  4687  preq12bg  4813  uniprg  4888  disji2  5092  disjprg  5104  disjxun  5106  axprg  5402  swopolem  5576  sotrieq  5597  isso2i  5603  dmopab2rex  5911  somin1  6145  ordequn  6494  fununi  6645  unima  6991  unpreima  7094  eqfunresadj  7401  ordsucun  7870  funcnvuni  7978  fiunlem  7988  frxp  8175  xporderlem  8176  poxp  8177  fnwelem  8180  fnwe2lem1  8182  fnse  8187  xpord2lem  8196  poxp2  8197  xpord3lem  8203  poxp3  8204  soseq  8213  oacan  8594  omword  8616  oeword  8637  oeoa  8644  qsdisj  8853  wemapso2lem  9583  brwdom  9598  cantnflem1  9727  r0weon  10130  infxpen  10132  sornom  10394  fin1ai  10410  isfin5  10416  isfin6  10417  sdom2en01  10419  enfin2i  10438  enfin1ai  10501  isfin5-2  10508  fin1a2lem7  10523  fin1a2lem11  10527  fin1a2lem13  10529  axdc3lem2  10568  engch  10752  eltskg  10874  tsken  10878  ltsonq  11093  addcanpr  11170  ltsosr  11218  axpre-lttri  11289  lemul1  12209  mulge0b  12227  mulle0b  12228  mulsuble0b  12229  nn1m1nn  12396  avgle  12628  nn0sub  12696  elznn0  12748  elz2  12751  nneo  12823  uztric  13029  mul2lt0bi  13268  ltxr  13284  xrrebnd  13338  xmulval  13395  xmulneg1  13439  ixxun  13532  iccsplit  13656  fzsplit2  13723  uzsplit  13770  nelfzo  13839  fzospliti  13866  fzouzsplit  13869  sqeqor  14401  swrdnd  14846  sumeq1  15900  sumeq2w  15903  sumeq2ii  15904  sumeq2sdv  15914  fz1f1o  15920  summo  15927  fsum  15930  prodeq1f  16119  prodeq1  16120  prodeq2w  16123  prodeq2ii  16124  prodeq2sdv  16135  prodmo  16147  fprod  16152  ruclem12  16453  odd2np1lem  16554  dvdsprime  16906  coprm  16931  vdwapun  17196  vdwlem6  17208  vdwlem10  17212  mreexexlemd  17868  mreexexd  17872  istos  18640  tosso  18641  tleile  18643  resstos  18654  tsrlin  18809  tsrss  18813  islring  20843  isdomn  21008  unichnlidl  21567  isprmidl  21670  prmidlc  21680  qsidomlem1  21687  qsidomlem2  21688  prmirredlem  21833  domnchr  21893  zntoslem  21917  znfld  21921  fctop  23377  cctop  23379  ppttop  23380  pptbas  23381  isufil  24277  ufilss  24279  fixufil  24296  fin1aufil  24306  xpsdsval  24755  nlmmul0or  25057  pmltpclem1  25824  iundisj2  25925  mbfmax  26025  dvne0  26386  fta1glem2  26542  plymul0or  26654  ofmulrt  26655  quotval  26668  plydivlem3  26671  plydivlem4  26672  plydivex  26673  plydivalg  26675  quotlem  26676  aalioulem2  26717  quad2  27224  dcubic2  27229  dcubic  27231  dquartlem1  27236  dquart  27238  quart  27246  leibpilem2  27326  wilthlem1  27452  muval2  27518  perfectlem2  27614  lgslem1  27681  pntpbnd1  27970  leslss  28352  abssor  28689  n0s0suc  28785  n0s0m1  28805  nn1m1nns  28817  elzn0s  28841  elzs2  28842  zsoring  28852  n0seo  28864  zseo  28865  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  bdayfinbnd  28912  z12zsodd  28925  legtrid  29111  legso  29119  ishlg2  29122  ishlg  29125  lnhl  29138  symquadlem  29218  plngcplem  29320  islmib  29349  isinag  29414  isinagd  29415  inaghl  29421  brprlng  29473  brbtwn2  29540  axcontlem2  29600  axcontlem4  29602  axcontlem11  29609  edglnl  29778  nb3grprlem2  30019  hashecclwwlkn1  30725  nfrgr2v  30930  h1datom  32241  atss  33005  atom1d  33012  atord  33047  chirred  33054  elimifd  33237  disji2f  33269  disjif2  33273  disjxpin  33280  iundisj2f  33282  disjunsn  33286  brprop  33387  quad3d  33437  fzsplit3  33481  iundisj2fi  33485  f1ocnt  33488  trleile  33628  domnpropd  33940  subrdom  33945  fldedom  33956  ply1edom  33959  mxidlmax  34094  rprmval  34152  isrprm  34153  smatrcl  34539  fsumcvg4  34693  dfac16  35887  brlexod  36040  brr0d  36042  onprcf1of1orbd  36095  onprcf1of1ord  36096  erdsze2lem2  36177  satf  36326  satfv1  36336  satfbrsuc  36339  satfrnmapom  36343  satf0op  36350  sat1el2xp  36352  fmlafvel  36358  fmlasuc  36359  fmla1  36360  isfmlasuc  36361  fmlaomn0  36363  fmlasucdisj  36372  satffunlem1lem1  36375  satffunlem1lem2  36376  satffunlem2lem1  36377  dmopab3rexdif  36378  satffunlem2lem2  36379  satfv1fvfmla1  36396  2goelgoanfmla1  36397  satefvfmla1  36398  funpsstri  36746  seglelin  37096  lineunray  37127  ltnadd  37182  naddle  37183  prodeq12sdv  37222  cbvsumdavw  37283  cbvproddavw  37284  cbvsumdavw2  37299  cbvproddavw2  37300  weiunval  37465  axtcond  37481  topdifinffinlem  38538  topdifinffin  38539  topdifinfeq  38541  mblfinlem2  38844  itg2addnclem2  38858  iblabsnclem  38869  ftc1anclem5  38883  fdc1  38946  unichnidl  39231  ispridl  39234  maxidlmax  39243  disjressuc2  39609  qsdisjALTV  39897  lcvexchlem4  40360  lcvexchlem5  40361  2at0mat0  40848  pmapjoin  41175  cdlemg17h  41991  dihlspsnat  42656  quadfac  43521  lzunuz  44045  dvdsrabdioph  44083  acongeq12d  44252  jm2.25  44272  rmydioph  44287  expdioph  44296  aomclem8  44329  fzunt  44717  fzuntd  44718  fzunt1d  44719  fzuntgd  44720  sqrtcvallem1  44892  brfvrcld2  44953  uneqsn  45286  ntrneixb  45356  ntrneix3  45358  ntrneix13  45360  mnringmulrcld  45487  disjinfi  46480  salexct  47617  salexct2  47622  salexct3  47625  salgencntex  47626  salgensscntex  47627  nnfoctbdjlem  47738  nnfoctbdj  47739  iundjiun  47743  opprb  48374  euoreqb  48453  el1fzopredsuc  48669  iccpartgel  48784  paireqne  48866  divgcdoddALTV  49053  perfectALTVlem2  49093  clnbgrel  49199  dfvopnbgr2  49224  vopnbgrel  49225  dfclnbgr6  49227  dfnbgr6  49228  clnbgrgrim  49305  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg5edgnedg  49501  lindslinindsimp2lem5  49905  ldepspr  49916  prelrrx2b  50158  rrx2pnedifcoorneor  50160  rrx2plord  50164  rrx2plordisom  50167  itsclc0yqsol  50207