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  1095  3orbi123d  1463  cadbi123d  1640  eueq3  3675  sbcor  3795  unjust  3910  elun  4108  elprg  4613  eltpg  4653  el7g  4657  reuprg0  4669  rabsnifsb  4689  rabrsn  4691  preq12bg  4819  uniprg  4889  disji2  5094  disjprg  5106  disjxun  5108  axprg  5410  swopolem  5581  sotrieq  5602  isso2i  5608  dmopab2rex  5909  somin1  6135  ordequn  6468  fununi  6613  unima  6958  unpreima  7060  eqfunresadj  7360  ordsucun  7822  funcnvuni  7930  fiunlem  7940  frxp  8123  xporderlem  8124  poxp  8125  fnwelem  8128  fnse  8130  xpord2lem  8139  poxp2  8140  xpord3lem  8146  poxp3  8147  soseq  8156  oacan  8534  omword  8556  oeword  8577  oeoa  8584  qsdisj  8793  wemapso2lem  9515  brwdom  9530  cantnflem1  9659  r0weon  9997  infxpen  9999  sornom  10262  fin1ai  10278  isfin5  10284  isfin6  10285  sdom2en01  10287  enfin2i  10306  enfin1ai  10369  isfin5-2  10376  fin1a2lem7  10391  fin1a2lem11  10395  fin1a2lem13  10397  axdc3lem2  10436  engch  10614  eltskg  10736  tsken  10740  ltsonq  10955  addcanpr  11032  ltsosr  11080  axpre-lttri  11151  lemul1  12068  mulge0b  12086  mulle0b  12087  mulsuble0b  12088  nn1m1nn  12255  avgle  12487  nn0sub  12555  elznn0  12607  elz2  12610  nneo  12681  uztric  12887  mul2lt0bi  13125  ltxr  13141  xrrebnd  13195  xmulval  13252  xmulneg1  13296  ixxun  13389  iccsplit  13513  fzsplit2  13579  uzsplit  13626  nelfzo  13695  fzospliti  13722  fzouzsplit  13725  sqeqor  14254  swrdnd  14694  sumeq1  15742  sumeq2w  15745  sumeq2ii  15746  sumeq2sdv  15756  fz1f1o  15763  summo  15770  fsum  15773  prodeq1f  15962  prodeq1  15963  prodeq2w  15966  prodeq2ii  15967  prodeq2sdv  15979  prodmo  15992  fprod  15997  ruclem12  16298  odd2np1lem  16399  dvdsprime  16746  coprm  16771  vdwapun  17035  vdwlem6  17047  vdwlem10  17051  mreexexlemd  17701  mreexexd  17705  istos  18473  tosso  18474  tleile  18476  resstos  18487  tsrlin  18642  tsrss  18646  islring  20626  isdomn  20791  unichnlidl  21343  isprmidl  21444  prmidlc  21454  qsidomlem1  21461  qsidomlem2  21462  prmirredlem  21603  domnchr  21663  zntoslem  21687  znfld  21691  fctop  23142  cctop  23144  ppttop  23145  pptbas  23146  isufil  24041  ufilss  24043  fixufil  24060  fin1aufil  24070  xpsdsval  24519  nlmmul0or  24821  pmltpclem1  25588  iundisj2  25689  mbfmax  25789  dvne0  26151  fta1glem2  26307  plymul0or  26420  ofmulrt  26421  quotval  26434  plydivlem3  26437  plydivlem4  26438  plydivex  26439  plydivalg  26441  quotlem  26442  aalioulem2  26477  quad2  26985  dcubic2  26990  dcubic  26992  dquartlem1  26997  dquart  26999  quart  27007  leibpilem2  27087  wilthlem1  27213  muval2  27279  perfectlem2  27375  lgslem1  27442  pntpbnd1  27731  leslss  28083  abssor  28420  n0s0suc  28516  n0s0m1  28536  nn1m1nns  28548  elzn0s  28572  elzs2  28573  zsoring  28583  n0seo  28595  zseo  28596  bdayfinbndcbv  28640  bdayfinbndlem1  28641  bdayfinbndlem2  28642  bdayfinbnd  28643  z12zsodd  28656  legtrid  28841  legso  28849  ishlg2  28852  ishlg  28855  lnhl  28868  symquadlem  28947  plngcplem  29048  islmib  29077  isinag  29136  isinagd  29137  inaghl  29143  brprlng  29169  brbtwn2  29236  axcontlem2  29296  axcontlem4  29298  axcontlem11  29305  edglnl  29474  nb3grprlem2  29712  hashecclwwlkn1  30409  nfrgr2v  30604  h1datom  31915  atss  32679  atom1d  32686  atord  32721  chirred  32728  elimifd  32870  disji2f  32903  disjif2  32907  disjxpin  32914  iundisj2f  32916  disjunsn  32920  brprop  33023  quad3d  33075  fzsplit3  33119  iundisj2fi  33123  f1ocnt  33126  trleile  33272  domnpropd  33581  subrdom  33586  mxidlmax  33729  rprmval  33787  isrprm  33788  smatrcl  34167  fsumcvg4  34321  erdsze2lem2  35677  satf  35826  satfv1  35836  satfbrsuc  35839  satfrnmapom  35843  satf0op  35850  sat1el2xp  35852  fmlafvel  35858  fmlasuc  35859  fmla1  35860  isfmlasuc  35861  fmlaomn0  35863  fmlasucdisj  35872  satffunlem1lem1  35875  satffunlem1lem2  35876  satffunlem2lem1  35877  dmopab3rexdif  35878  satffunlem2lem2  35879  satfv1fvfmla1  35896  2goelgoanfmla1  35897  satefvfmla1  35898  funpsstri  36239  seglelin  36589  lineunray  36620  ltnadd  36676  naddle  36677  prodeq12sdv  36711  cbvsumdavw  36772  cbvproddavw  36773  cbvsumdavw2  36788  cbvproddavw2  36789  weiunval  36954  axtcond  36970  topdifinffinlem  37974  topdifinffin  37975  topdifinfeq  37977  mblfinlem2  38290  itg2addnclem2  38304  iblabsnclem  38315  ftc1anclem5  38329  fdc1  38378  unichnidl  38663  ispridl  38666  maxidlmax  38675  disjressuc2  39041  qsdisjALTV  39329  lcvexchlem4  39792  lcvexchlem5  39793  2at0mat0  40280  pmapjoin  40607  cdlemg17h  41423  dihlspsnat  42088  quadfac  42953  lzunuz  43482  dvdsrabdioph  43520  acongeq12d  43689  jm2.25  43709  rmydioph  43724  expdioph  43733  fnwe2val  43759  aomclem8  43771  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  sqrtcvallem1  44340  brfvrcld2  44401  uneqsn  44734  ntrneixb  44804  ntrneix3  44806  ntrneix13  44808  mnringmulrcld  44935  disjinfi  45893  salexct  47031  salexct2  47036  salexct3  47039  salgencntex  47040  salgensscntex  47041  nnfoctbdjlem  47152  nnfoctbdj  47153  iundjiun  47157  opprb  47751  euoreqb  47829  el1fzopredsuc  48046  iccpartgel  48161  paireqne  48243  divgcdoddALTV  48430  perfectALTVlem2  48470  clnbgrel  48576  dfvopnbgr2  48601  vopnbgrel  48602  dfclnbgr6  48604  dfnbgr6  48605  clnbgrgrim  48682  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpg5edgnedg  48878  lindslinindsimp2lem5  49225  ldepspr  49236  rrx2pnedifcoorneor  49479  rrx2plord  49483  rrx2plordisom  49486  itsclc0yqsol  49527