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 281	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208   ∨ 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 209  df-or 844

This theorem is referenced by:  pm4.39  973  ifpbi123d  1072  ifpbi123dOLD  1073  3orbi123d  1431  cadbi123d  1611  eueq3  3702  sbcor  3822  unjust  3940  elun  4125  elprg  4588  eltpg  4623  reuprg0  4638  rabsnifsb  4658  rabrsn  4660  preq12bg  4784  disji2  5048  disjprgw  5061  disjprg  5062  disjxun  5064  swopolem  5483  sotrieq  5502  isso2i  5508  dmopab2rex  5786  somin1  5993  ordequn  6291  fununi  6429  unima  6739  unpreima  6833  ordsucun  7540  funcnvuni  7636  fiunlem  7643  frxp  7820  xporderlem  7821  poxp  7822  fnwelem  7825  fnse  7827  oacan  8174  omword  8196  oeword  8216  oeoa  8223  qsdisj  8374  wemapso2lem  9016  brwdom  9031  cantnflem1  9152  r0weon  9438  infxpen  9440  sornom  9699  fin1ai  9715  isfin5  9721  isfin6  9722  sdom2en01  9724  enfin2i  9743  enfin1ai  9806  isfin5-2  9813  fin1a2lem7  9828  fin1a2lem11  9832  fin1a2lem13  9834  axdc3lem2  9873  engch  10050  eltskg  10172  tsken  10176  ltsonq  10391  addcanpr  10468  ltsosr  10516  axpre-lttri  10587  lemul1  11492  mulge0b  11510  mulle0b  11511  mulsuble0b  11512  nn1m1nn  11659  avgle  11880  nn0sub  11948  elznn0  11997  elz2  12000  nneo  12067  uztric  12267  mul2lt0bi  12496  ltxr  12511  xrrebnd  12562  xmulval  12619  xmulneg1  12663  ixxun  12755  iccsplit  12872  fzsplit2  12933  uzsplit  12980  nelfzo  13044  fzospliti  13070  fzouzsplit  13073  sqeqor  13579  swrdnd  14016  sumeq1  15045  sumeq2w  15049  sumeq2ii  15050  fz1f1o  15067  summo  15074  fsum  15077  prodeq1f  15262  prodeq2w  15266  prodeq2ii  15267  prodmo  15290  fprod  15295  ruclem12  15594  odd2np1lem  15689  dvdsprime  16031  coprm  16055  vdwapun  16310  vdwlem6  16322  vdwlem10  16326  mreexexlemd  16915  mreexexd  16919  istos  17645  tosso  17646  tsrlin  17829  tsrss  17833  isdomn  20067  prmirredlem  20640  domnchr  20679  zntoslem  20703  znfld  20707  fctop  21612  cctop  21614  ppttop  21615  pptbas  21616  isufil  22511  ufilss  22513  fixufil  22530  fin1aufil  22540  xpsdsval  22991  nlmmul0or  23292  pmltpclem1  24049  iundisj2  24150  mbfmax  24250  dvne0  24608  fta1glem2  24760  plymul0or  24870  ofmulrt  24871  quotval  24881  plydivlem3  24884  plydivlem4  24885  plydivex  24886  plydivalg  24888  quotlem  24889  aalioulem2  24922  quad2  25417  dcubic2  25422  dcubic  25424  dquartlem1  25429  dquart  25431  quart  25439  leibpilem2  25519  wilthlem1  25645  muval2  25711  perfectlem2  25806  lgslem1  25873  pntpbnd1  26162  legtrid  26377  legso  26385  ishlg  26388  lnhl  26401  symquadlem  26475  islmib  26573  isinag  26624  isinagd  26625  inaghl  26631  brbtwn2  26691  axcontlem2  26751  axcontlem4  26753  axcontlem11  26760  edglnl  26928  nb3grprlem2  27163  hashecclwwlkn1  27856  nfrgr2v  28051  h1datom  29359  atss  30123  atom1d  30130  atord  30165  chirred  30172  elimifd  30298  disji2f  30327  disjif2  30331  disjxpin  30338  iundisj2f  30340  disjunsn  30344  brprop  30433  fzsplit3  30517  iundisj2fi  30520  f1ocnt  30525  resstos  30647  tleile  30648  trleile  30653  isprmidl  30955  prmidlc  30964  qsidomlem1  30965  qsidomlem2  30966  mxidlmax  30974  smatrcl  31061  fsumcvg4  31193  erdsze2lem2  32451  satf  32600  satfv1  32610  satfbrsuc  32613  satfrnmapom  32617  satf0op  32624  sat1el2xp  32626  fmlafvel  32632  fmlasuc  32633  fmla1  32634  isfmlasuc  32635  fmlaomn0  32637  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem1lem2  32650  satffunlem2lem1  32651  dmopab3rexdif  32652  satffunlem2lem2  32653  satfv1fvfmla1  32670  2goelgoanfmla1  32671  satefvfmla1  32672  eqfunresadj  33004  funpsstri  33008  soseq  33096  seglelin  33577  lineunray  33608  topdifinffinlem  34631  topdifinffin  34632  topdifinfeq  34634  mblfinlem2  34945  itg2addnclem2  34959  iblabsnclem  34970  ftc1anclem5  34986  fdc1  35036  unichnidl  35324  ispridl  35327  maxidlmax  35336  qsdisjALTV  35865  lcvexchlem4  36188  lcvexchlem5  36189  2at0mat0  36676  pmapjoin  37003  cdlemg17h  37819  dihlspsnat  38484  lzunuz  39414  dvdsrabdioph  39456  acongeq12d  39625  jm2.25  39645  rmydioph  39660  expdioph  39669  fnwe2val  39698  aomclem8  39710  brfvrcld2  40086  uneqsn  40422  ntrneixb  40494  ntrneix3  40496  ntrneix13  40498  disjinfi  41503  salexct  42666  salexct2  42671  salexct3  42674  salgencntex  42675  salgensscntex  42676  nnfoctbdjlem  42786  nnfoctbdj  42787  iundjiun  42791  opprb  43315  euoreqb  43357  el1fzopredsuc  43574  iccpartgel  43638  paireqne  43722  divgcdoddALTV  43896  perfectALTVlem2  43936  lindslinindsimp2lem5  44566  ldepspr  44577  rrx2pnedifcoorneor  44752  rrx2plord  44756  rrx2plordisom  44759  itsclc0yqsol  44800