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  1463  cadbi123d  1642  eueq3  3668  sbcor  3788  unjust  4150  elun  4152  elprg  4603  eltpg  4643  el7g  4647  reuprg0  4659  rabsnifsb  4679  rabrsn  4681  preq12bg  4807  uniprg  4882  disji2  5086  disjprg  5098  disjxun  5100  axprg  5394  swopolem  5568  sotrieq  5589  isso2i  5595  dmopab2rex  5898  somin1  6126  ordequn  6468  fununi  6616  unima  6961  unpreima  7063  eqfunresadj  7371  ordsucun  7837  funcnvuni  7945  fiunlem  7955  frxp  8141  xporderlem  8142  poxp  8143  fnwelem  8146  fnwe2lem1  8148  fnse  8153  xpord2lem  8162  poxp2  8163  xpord3lem  8169  poxp3  8170  soseq  8179  oacan  8560  omword  8582  oeword  8603  oeoa  8610  qsdisj  8819  wemapso2lem  9550  brwdom  9565  cantnflem1  9694  r0weon  10095  infxpen  10097  sornom  10359  fin1ai  10375  isfin5  10381  isfin6  10382  sdom2en01  10384  enfin2i  10403  enfin1ai  10466  isfin5-2  10473  fin1a2lem7  10488  fin1a2lem11  10492  fin1a2lem13  10494  axdc3lem2  10533  engch  10717  eltskg  10839  tsken  10843  ltsonq  11058  addcanpr  11135  ltsosr  11183  axpre-lttri  11254  lemul1  12173  mulge0b  12191  mulle0b  12192  mulsuble0b  12193  nn1m1nn  12360  avgle  12592  nn0sub  12660  elznn0  12712  elz2  12715  nneo  12787  uztric  12993  mul2lt0bi  13232  ltxr  13248  xrrebnd  13302  xmulval  13359  xmulneg1  13403  ixxun  13496  iccsplit  13620  fzsplit2  13687  uzsplit  13734  nelfzo  13803  fzospliti  13830  fzouzsplit  13833  sqeqor  14364  swrdnd  14809  sumeq1  15862  sumeq2w  15865  sumeq2ii  15866  sumeq2sdv  15876  fz1f1o  15882  summo  15889  fsum  15892  prodeq1f  16081  prodeq1  16082  prodeq2w  16085  prodeq2ii  16086  prodeq2sdv  16097  prodmo  16109  fprod  16114  ruclem12  16415  odd2np1lem  16516  dvdsprime  16868  coprm  16893  vdwapun  17158  vdwlem6  17170  vdwlem10  17174  mreexexlemd  17824  mreexexd  17828  istos  18596  tosso  18597  tleile  18599  resstos  18610  tsrlin  18765  tsrss  18769  islring  20798  isdomn  20963  unichnlidl  21522  isprmidl  21625  prmidlc  21635  qsidomlem1  21642  qsidomlem2  21643  prmirredlem  21784  domnchr  21844  zntoslem  21868  znfld  21872  fctop  23328  cctop  23330  ppttop  23331  pptbas  23332  isufil  24228  ufilss  24230  fixufil  24247  fin1aufil  24257  xpsdsval  24706  nlmmul0or  25008  pmltpclem1  25775  iundisj2  25876  mbfmax  25976  dvne0  26337  fta1glem2  26493  plymul0or  26605  ofmulrt  26606  quotval  26619  plydivlem3  26622  plydivlem4  26623  plydivex  26624  plydivalg  26626  quotlem  26627  aalioulem2  26666  quad2  27173  dcubic2  27178  dcubic  27180  dquartlem1  27185  dquart  27187  quart  27195  leibpilem2  27275  wilthlem1  27401  muval2  27467  perfectlem2  27563  lgslem1  27630  pntpbnd1  27919  leslss  28301  abssor  28638  n0s0suc  28734  n0s0m1  28754  nn1m1nns  28766  elzn0s  28790  elzs2  28791  zsoring  28801  n0seo  28813  zseo  28814  bdayfinbndcbv  28858  bdayfinbndlem1  28859  bdayfinbndlem2  28860  bdayfinbnd  28861  z12zsodd  28874  legtrid  29060  legso  29068  ishlg2  29071  ishlg  29074  lnhl  29087  symquadlem  29167  plngcplem  29269  islmib  29298  isinag  29363  isinagd  29364  inaghl  29370  brprlng  29422  brbtwn2  29489  axcontlem2  29549  axcontlem4  29551  axcontlem11  29558  edglnl  29727  nb3grprlem2  29968  hashecclwwlkn1  30674  nfrgr2v  30879  h1datom  32190  atss  32954  atom1d  32961  atord  32996  chirred  33003  elimifd  33187  disji2f  33219  disjif2  33223  disjxpin  33230  iundisj2f  33232  disjunsn  33236  brprop  33338  quad3d  33388  fzsplit3  33432  iundisj2fi  33436  f1ocnt  33439  trleile  33579  domnpropd  33888  subrdom  33893  mxidlmax  34037  rprmval  34095  isrprm  34096  smatrcl  34475  fsumcvg4  34629  dfac16  35811  brlexod  35939  brr0d  35941  onprcf1of1orbd  35974  onprcf1of1ord  35975  erdsze2lem2  36056  satf  36205  satfv1  36215  satfbrsuc  36218  satfrnmapom  36222  satf0op  36229  sat1el2xp  36231  fmlafvel  36237  fmlasuc  36238  fmla1  36239  isfmlasuc  36240  fmlaomn0  36242  fmlasucdisj  36251  satffunlem1lem1  36254  satffunlem1lem2  36255  satffunlem2lem1  36256  dmopab3rexdif  36257  satffunlem2lem2  36258  satfv1fvfmla1  36275  2goelgoanfmla1  36276  satefvfmla1  36277  funpsstri  36624  seglelin  36974  lineunray  37005  ltnadd  37060  naddle  37061  prodeq12sdv  37100  cbvsumdavw  37161  cbvproddavw  37162  cbvsumdavw2  37177  cbvproddavw2  37178  weiunval  37343  axtcond  37359  topdifinffinlem  38364  topdifinffin  38365  topdifinfeq  38367  mblfinlem2  38670  itg2addnclem2  38684  iblabsnclem  38695  ftc1anclem5  38709  fdc1  38774  unichnidl  39059  ispridl  39062  maxidlmax  39071  disjressuc2  39437  qsdisjALTV  39725  lcvexchlem4  40188  lcvexchlem5  40189  2at0mat0  40676  pmapjoin  41003  cdlemg17h  41819  dihlspsnat  42484  quadfac  43349  lzunuz  43873  dvdsrabdioph  43911  acongeq12d  44080  jm2.25  44100  rmydioph  44115  expdioph  44124  aomclem8  44157  fzunt  44550  fzuntd  44551  fzunt1d  44552  fzuntgd  44553  sqrtcvallem1  44725  brfvrcld2  44786  uneqsn  45119  ntrneixb  45189  ntrneix3  45191  ntrneix13  45193  mnringmulrcld  45320  disjinfi  46301  salexct  47438  salexct2  47443  salexct3  47446  salgencntex  47447  salgensscntex  47448  nnfoctbdjlem  47559  nnfoctbdj  47560  iundjiun  47564  opprb  48195  euoreqb  48273  el1fzopredsuc  48490  iccpartgel  48605  paireqne  48687  divgcdoddALTV  48874  perfectALTVlem2  48914  clnbgrel  49020  dfvopnbgr2  49045  vopnbgrel  49046  dfclnbgr6  49048  dfnbgr6  49049  clnbgrgrim  49126  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg5edgnedg  49322  lindslinindsimp2lem5  49668  ldepspr  49679  prelrrx2b  49921  rrx2pnedifcoorneor  49923  rrx2plord  49927  rrx2plordisom  49930  itsclc0yqsol  49970