Theorem orbi12d 915

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  pm4.39  973  ifpbi123d  1076  ifpbi123dOLD  1077  3orbi123d  1433  cadbi123d  1613  eueq3  3641  sbcor  3764  unjust  3887  elun  4079  elprg  4579  eltpg  4618  reuprg0  4635  rabsnifsb  4655  rabrsn  4657  preq12bg  4781  uniprg  4853  disji2  5052  disjprgw  5065  disjprg  5066  disjxun  5068  swopolem  5504  sotrieq  5523  isso2i  5529  dmopab2rex  5815  somin1  6027  ordequn  6351  fununi  6493  unima  6825  unpreima  6922  ordsucun  7647  funcnvuni  7752  fiunlem  7758  frxp  7938  xporderlem  7939  poxp  7940  fnwelem  7943  fnse  7945  oacan  8341  omword  8363  oeword  8383  oeoa  8390  qsdisj  8541  wemapso2lem  9241  brwdom  9256  cantnflem1  9377  r0weon  9699  infxpen  9701  sornom  9964  fin1ai  9980  isfin5  9986  isfin6  9987  sdom2en01  9989  enfin2i  10008  enfin1ai  10071  isfin5-2  10078  fin1a2lem7  10093  fin1a2lem11  10097  fin1a2lem13  10099  axdc3lem2  10138  engch  10315  eltskg  10437  tsken  10441  ltsonq  10656  addcanpr  10733  ltsosr  10781  axpre-lttri  10852  lemul1  11757  mulge0b  11775  mulle0b  11776  mulsuble0b  11777  nn1m1nn  11924  avgle  12145  nn0sub  12213  elznn0  12264  elz2  12267  nneo  12334  uztric  12535  mul2lt0bi  12765  ltxr  12780  xrrebnd  12831  xmulval  12888  xmulneg1  12932  ixxun  13024  iccsplit  13146  fzsplit2  13210  uzsplit  13257  nelfzo  13321  fzospliti  13347  fzouzsplit  13350  sqeqor  13860  swrdnd  14295  sumeq1  15328  sumeq2w  15332  sumeq2ii  15333  fz1f1o  15350  summo  15357  fsum  15360  prodeq1f  15546  prodeq2w  15550  prodeq2ii  15551  prodmo  15574  fprod  15579  ruclem12  15878  odd2np1lem  15977  dvdsprime  16320  coprm  16344  vdwapun  16603  vdwlem6  16615  vdwlem10  16619  mreexexlemd  17270  mreexexd  17274  istos  18051  tosso  18052  tleile  18054  tsrlin  18218  tsrss  18222  isdomn  20478  prmirredlem  20606  domnchr  20648  zntoslem  20676  znfld  20680  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  isufil  22962  ufilss  22964  fixufil  22981  fin1aufil  22991  xpsdsval  23442  nlmmul0or  23753  pmltpclem1  24517  iundisj2  24618  mbfmax  24718  dvne0  25080  fta1glem2  25236  plymul0or  25346  ofmulrt  25347  quotval  25357  plydivlem3  25360  plydivlem4  25361  plydivex  25362  plydivalg  25364  quotlem  25365  aalioulem2  25398  quad2  25894  dcubic2  25899  dcubic  25901  dquartlem1  25906  dquart  25908  quart  25916  leibpilem2  25996  wilthlem1  26122  muval2  26188  perfectlem2  26283  lgslem1  26350  pntpbnd1  26639  legtrid  26856  legso  26864  ishlg  26867  lnhl  26880  symquadlem  26954  islmib  27052  isinag  27103  isinagd  27104  inaghl  27110  brbtwn2  27176  axcontlem2  27236  axcontlem4  27238  axcontlem11  27245  edglnl  27416  nb3grprlem2  27651  hashecclwwlkn1  28342  nfrgr2v  28537  h1datom  29845  atss  30609  atom1d  30616  atord  30651  chirred  30658  elimifd  30787  disji2f  30817  disjif2  30821  disjxpin  30828  iundisj2f  30830  disjunsn  30834  brprop  30932  fzsplit3  31017  iundisj2fi  31020  f1ocnt  31025  resstos  31147  trleile  31151  isprmidl  31515  prmidlc  31526  qsidomlem1  31530  qsidomlem2  31531  mxidlmax  31539  rprmval  31566  isrprm  31567  smatrcl  31648  fsumcvg4  31802  erdsze2lem2  33066  satf  33215  satfv1  33225  satfbrsuc  33228  satfrnmapom  33232  satf0op  33239  sat1el2xp  33241  fmlafvel  33247  fmlasuc  33248  fmla1  33249  isfmlasuc  33250  fmlaomn0  33252  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem1lem2  33265  satffunlem2lem1  33266  dmopab3rexdif  33267  satffunlem2lem2  33268  satfv1fvfmla1  33285  2goelgoanfmla1  33286  satefvfmla1  33287  eqfunresadj  33641  funpsstri  33645  xpord2lem  33716  poxp2  33717  xpord3lem  33722  poxp3  33723  soseq  33730  seglelin  34345  lineunray  34376  topdifinffinlem  35445  topdifinffin  35446  topdifinfeq  35448  mblfinlem2  35742  itg2addnclem2  35756  iblabsnclem  35767  ftc1anclem5  35781  fdc1  35831  unichnidl  36116  ispridl  36119  maxidlmax  36128  qsdisjALTV  36655  lcvexchlem4  36978  lcvexchlem5  36979  2at0mat0  37466  pmapjoin  37793  cdlemg17h  38609  dihlspsnat  39274  lzunuz  40506  dvdsrabdioph  40548  acongeq12d  40717  jm2.25  40737  rmydioph  40752  expdioph  40761  fnwe2val  40790  aomclem8  40802  sqrtcvallem1  41128  brfvrcld2  41189  uneqsn  41522  ntrneixb  41594  ntrneix3  41596  ntrneix13  41598  mnringmulrcld  41735  disjinfi  42620  salexct  43763  salexct2  43768  salexct3  43771  salgencntex  43772  salgensscntex  43773  nnfoctbdjlem  43883  nnfoctbdj  43884  iundjiun  43888  opprb  44412  euoreqb  44488  el1fzopredsuc  44705  iccpartgel  44769  paireqne  44851  divgcdoddALTV  45022  perfectALTVlem2  45062  lindslinindsimp2lem5  45691  ldepspr  45702  rrx2pnedifcoorneor  45950  rrx2plord  45954  rrx2plordisom  45957  itsclc0yqsol  45998