Theorem orbi12d 917

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

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

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 846

This theorem is referenced by:  pm4.39  975  ifpbi123d  1078  ifpbi123dOLD  1079  3orbi123d  1435  cadbi123d  1611  eueq3  3707  sbcor  3830  unjust  3952  elun  4148  elprg  4649  eltpg  4689  reuprg0  4706  rabsnifsb  4726  rabrsn  4728  preq12bg  4854  uniprg  4925  disji2  5130  disjprgw  5143  disjprg  5144  disjxun  5146  swopolem  5598  sotrieq  5617  isso2i  5623  dmopab2rex  5917  somin1  6134  ordequn  6467  fununi  6623  unima  6966  unpreima  7064  eqfunresadj  7356  ordsucun  7812  funcnvuni  7921  fiunlem  7927  frxp  8111  xporderlem  8112  poxp  8113  fnwelem  8116  fnse  8118  xpord2lem  8127  poxp2  8128  xpord3lem  8134  poxp3  8135  soseq  8144  oacan  8547  omword  8569  oeword  8589  oeoa  8596  qsdisj  8787  wemapso2lem  9546  brwdom  9561  cantnflem1  9683  r0weon  10006  infxpen  10008  sornom  10271  fin1ai  10287  isfin5  10293  isfin6  10294  sdom2en01  10296  enfin2i  10315  enfin1ai  10378  isfin5-2  10385  fin1a2lem7  10400  fin1a2lem11  10404  fin1a2lem13  10406  axdc3lem2  10445  engch  10622  eltskg  10744  tsken  10748  ltsonq  10963  addcanpr  11040  ltsosr  11088  axpre-lttri  11159  lemul1  12065  mulge0b  12083  mulle0b  12084  mulsuble0b  12085  nn1m1nn  12232  avgle  12453  nn0sub  12521  elznn0  12572  elz2  12575  nneo  12645  uztric  12845  mul2lt0bi  13079  ltxr  13094  xrrebnd  13146  xmulval  13203  xmulneg1  13247  ixxun  13339  iccsplit  13461  fzsplit2  13525  uzsplit  13572  nelfzo  13636  fzospliti  13663  fzouzsplit  13666  sqeqor  14179  swrdnd  14603  sumeq1  15634  sumeq2w  15637  sumeq2ii  15638  fz1f1o  15655  summo  15662  fsum  15665  prodeq1f  15851  prodeq2w  15855  prodeq2ii  15856  prodmo  15879  fprod  15884  ruclem12  16183  odd2np1lem  16282  dvdsprime  16623  coprm  16647  vdwapun  16906  vdwlem6  16918  vdwlem10  16922  mreexexlemd  17587  mreexexd  17591  istos  18370  tosso  18371  tleile  18373  tsrlin  18537  tsrss  18541  islring  20309  isdomn  20909  prmirredlem  21041  domnchr  21083  zntoslem  21111  znfld  21115  fctop  22506  cctop  22508  ppttop  22509  pptbas  22510  isufil  23406  ufilss  23408  fixufil  23425  fin1aufil  23435  xpsdsval  23886  nlmmul0or  24199  pmltpclem1  24964  iundisj2  25065  mbfmax  25165  dvne0  25527  fta1glem2  25683  plymul0or  25793  ofmulrt  25794  quotval  25804  plydivlem3  25807  plydivlem4  25808  plydivex  25809  plydivalg  25811  quotlem  25812  aalioulem2  25845  quad2  26341  dcubic2  26346  dcubic  26348  dquartlem1  26353  dquart  26355  quart  26363  leibpilem2  26443  wilthlem1  26569  muval2  26635  perfectlem2  26730  lgslem1  26797  pntpbnd1  27086  legtrid  27839  legso  27847  ishlg  27850  lnhl  27863  symquadlem  27937  islmib  28035  isinag  28086  isinagd  28087  inaghl  28093  brbtwn2  28160  axcontlem2  28220  axcontlem4  28222  axcontlem11  28229  edglnl  28400  nb3grprlem2  28635  hashecclwwlkn1  29327  nfrgr2v  29522  h1datom  30830  atss  31594  atom1d  31601  atord  31636  chirred  31643  elimifd  31770  disji2f  31803  disjif2  31807  disjxpin  31814  iundisj2f  31816  disjunsn  31820  brprop  31914  fzsplit3  32000  iundisj2fi  32003  f1ocnt  32008  resstos  32132  trleile  32136  isprmidl  32551  prmidlc  32562  qsidomlem1  32566  qsidomlem2  32567  mxidlmax  32576  rprmval  32628  isrprm  32629  smatrcl  32771  fsumcvg4  32925  erdsze2lem2  34190  satf  34339  satfv1  34349  satfbrsuc  34352  satfrnmapom  34356  satf0op  34363  sat1el2xp  34365  fmlafvel  34371  fmlasuc  34372  fmla1  34373  isfmlasuc  34374  fmlaomn0  34376  fmlasucdisj  34385  satffunlem1lem1  34388  satffunlem1lem2  34389  satffunlem2lem1  34390  dmopab3rexdif  34391  satffunlem2lem2  34392  satfv1fvfmla1  34409  2goelgoanfmla1  34410  satefvfmla1  34411  funpsstri  34732  seglelin  35083  lineunray  35114  topdifinffinlem  36223  topdifinffin  36224  topdifinfeq  36226  mblfinlem2  36521  itg2addnclem2  36535  iblabsnclem  36546  ftc1anclem5  36560  fdc1  36609  unichnidl  36894  ispridl  36897  maxidlmax  36906  disjressuc2  37253  qsdisjALTV  37480  lcvexchlem4  37902  lcvexchlem5  37903  2at0mat0  38391  pmapjoin  38718  cdlemg17h  39534  dihlspsnat  40199  lzunuz  41496  dvdsrabdioph  41538  acongeq12d  41708  jm2.25  41728  rmydioph  41743  expdioph  41752  fnwe2val  41781  aomclem8  41793  fzunt  42196  fzuntd  42197  fzunt1d  42198  fzuntgd  42199  sqrtcvallem1  42372  brfvrcld2  42433  uneqsn  42766  ntrneixb  42836  ntrneix3  42838  ntrneix13  42840  mnringmulrcld  42977  disjinfi  43881  salexct  45040  salexct2  45045  salexct3  45048  salgencntex  45049  salgensscntex  45050  nnfoctbdjlem  45161  nnfoctbdj  45162  iundjiun  45166  opprb  45731  euoreqb  45807  el1fzopredsuc  46023  iccpartgel  46087  paireqne  46169  divgcdoddALTV  46340  perfectALTVlem2  46380  lindslinindsimp2lem5  47133  ldepspr  47144  rrx2pnedifcoorneor  47392  rrx2plord  47396  rrx2plordisom  47399  itsclc0yqsol  47440