Theorem orbi12d 918

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

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

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 847

This theorem is referenced by:  pm4.39  976  ifpbi123d  1079  ifpbi123dOLD  1080  3orbi123d  1436  cadbi123d  1612  eueq3  3708  sbcor  3831  unjust  3953  elun  4149  elprg  4650  eltpg  4690  reuprg0  4707  rabsnifsb  4727  rabrsn  4729  preq12bg  4855  uniprg  4926  disji2  5131  disjprgw  5144  disjprg  5145  disjxun  5147  swopolem  5599  sotrieq  5618  isso2i  5624  dmopab2rex  5918  somin1  6135  ordequn  6468  fununi  6624  unima  6967  unpreima  7065  eqfunresadj  7357  ordsucun  7813  funcnvuni  7922  fiunlem  7928  frxp  8112  xporderlem  8113  poxp  8114  fnwelem  8117  fnse  8119  xpord2lem  8128  poxp2  8129  xpord3lem  8135  poxp3  8136  soseq  8145  oacan  8548  omword  8570  oeword  8590  oeoa  8597  qsdisj  8788  wemapso2lem  9547  brwdom  9562  cantnflem1  9684  r0weon  10007  infxpen  10009  sornom  10272  fin1ai  10288  isfin5  10294  isfin6  10295  sdom2en01  10297  enfin2i  10316  enfin1ai  10379  isfin5-2  10386  fin1a2lem7  10401  fin1a2lem11  10405  fin1a2lem13  10407  axdc3lem2  10446  engch  10623  eltskg  10745  tsken  10749  ltsonq  10964  addcanpr  11041  ltsosr  11089  axpre-lttri  11160  lemul1  12066  mulge0b  12084  mulle0b  12085  mulsuble0b  12086  nn1m1nn  12233  avgle  12454  nn0sub  12522  elznn0  12573  elz2  12576  nneo  12646  uztric  12846  mul2lt0bi  13080  ltxr  13095  xrrebnd  13147  xmulval  13204  xmulneg1  13248  ixxun  13340  iccsplit  13462  fzsplit2  13526  uzsplit  13573  nelfzo  13637  fzospliti  13664  fzouzsplit  13667  sqeqor  14180  swrdnd  14604  sumeq1  15635  sumeq2w  15638  sumeq2ii  15639  fz1f1o  15656  summo  15663  fsum  15666  prodeq1f  15852  prodeq2w  15856  prodeq2ii  15857  prodmo  15880  fprod  15885  ruclem12  16184  odd2np1lem  16283  dvdsprime  16624  coprm  16648  vdwapun  16907  vdwlem6  16919  vdwlem10  16923  mreexexlemd  17588  mreexexd  17592  istos  18371  tosso  18372  tleile  18374  tsrlin  18538  tsrss  18542  islring  20310  isdomn  20910  prmirredlem  21042  domnchr  21084  zntoslem  21112  znfld  21116  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  isufil  23407  ufilss  23409  fixufil  23426  fin1aufil  23436  xpsdsval  23887  nlmmul0or  24200  pmltpclem1  24965  iundisj2  25066  mbfmax  25166  dvne0  25528  fta1glem2  25684  plymul0or  25794  ofmulrt  25795  quotval  25805  plydivlem3  25808  plydivlem4  25809  plydivex  25810  plydivalg  25812  quotlem  25813  aalioulem2  25846  quad2  26344  dcubic2  26349  dcubic  26351  dquartlem1  26356  dquart  26358  quart  26366  leibpilem2  26446  wilthlem1  26572  muval2  26638  perfectlem2  26733  lgslem1  26800  pntpbnd1  27089  slelss  27403  legtrid  27873  legso  27881  ishlg  27884  lnhl  27897  symquadlem  27971  islmib  28069  isinag  28120  isinagd  28121  inaghl  28127  brbtwn2  28194  axcontlem2  28254  axcontlem4  28256  axcontlem11  28263  edglnl  28434  nb3grprlem2  28669  hashecclwwlkn1  29361  nfrgr2v  29556  h1datom  30866  atss  31630  atom1d  31637  atord  31672  chirred  31679  elimifd  31806  disji2f  31839  disjif2  31843  disjxpin  31850  iundisj2f  31852  disjunsn  31856  brprop  31950  fzsplit3  32036  iundisj2fi  32039  f1ocnt  32044  resstos  32168  trleile  32172  isprmidl  32587  prmidlc  32598  qsidomlem1  32602  qsidomlem2  32603  mxidlmax  32612  rprmval  32664  isrprm  32665  smatrcl  32807  fsumcvg4  32961  erdsze2lem2  34226  satf  34375  satfv1  34385  satfbrsuc  34388  satfrnmapom  34392  satf0op  34399  sat1el2xp  34401  fmlafvel  34407  fmlasuc  34408  fmla1  34409  isfmlasuc  34410  fmlaomn0  34412  fmlasucdisj  34421  satffunlem1lem1  34424  satffunlem1lem2  34425  satffunlem2lem1  34426  dmopab3rexdif  34427  satffunlem2lem2  34428  satfv1fvfmla1  34445  2goelgoanfmla1  34446  satefvfmla1  34447  funpsstri  34768  seglelin  35119  lineunray  35150  topdifinffinlem  36276  topdifinffin  36277  topdifinfeq  36279  mblfinlem2  36574  itg2addnclem2  36588  iblabsnclem  36599  ftc1anclem5  36613  fdc1  36662  unichnidl  36947  ispridl  36950  maxidlmax  36959  disjressuc2  37306  qsdisjALTV  37533  lcvexchlem4  37955  lcvexchlem5  37956  2at0mat0  38444  pmapjoin  38771  cdlemg17h  39587  dihlspsnat  40252  lzunuz  41554  dvdsrabdioph  41596  acongeq12d  41766  jm2.25  41786  rmydioph  41801  expdioph  41810  fnwe2val  41839  aomclem8  41851  fzunt  42254  fzuntd  42255  fzunt1d  42256  fzuntgd  42257  sqrtcvallem1  42430  brfvrcld2  42491  uneqsn  42824  ntrneixb  42894  ntrneix3  42896  ntrneix13  42898  mnringmulrcld  43035  disjinfi  43939  salexct  45098  salexct2  45103  salexct3  45106  salgencntex  45107  salgensscntex  45108  nnfoctbdjlem  45219  nnfoctbdj  45220  iundjiun  45224  opprb  45789  euoreqb  45865  el1fzopredsuc  46081  iccpartgel  46145  paireqne  46227  divgcdoddALTV  46398  perfectALTVlem2  46438  lindslinindsimp2lem5  47191  ldepspr  47202  rrx2pnedifcoorneor  47450  rrx2plord  47454  rrx2plordisom  47457  itsclc0yqsol  47498