Theorem orbi12d 913

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

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 842

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 208  df-or 843

This theorem is referenced by:  pm4.39  971  ifpbi123d  1070  3orbi123d  1427  cadbi123d  1592  eueq3  3638  sbcor  3751  unjust  3863  elun  4046  elprg  4493  eltpg  4530  reuprg0  4545  rabsnifsb  4565  rabrsn  4567  preq12bg  4691  disji2  4946  disjprg  4958  disjxun  4960  swopolem  5371  sotrieq  5390  isso2i  5396  dmopab2rex  5672  somin1  5869  ordequn  6166  fununi  6299  unpreima  6698  ordsucun  7396  funcnvuni  7492  fiunlem  7499  frxp  7673  xporderlem  7674  poxp  7675  fnwelem  7678  fnse  7680  oacan  8024  omword  8046  oeword  8066  oeoa  8073  qsdisj  8224  wemapso2lem  8862  brwdom  8877  cantnflem1  8998  r0weon  9284  infxpen  9286  sornom  9545  fin1ai  9561  isfin5  9567  isfin6  9568  sdom2en01  9570  enfin2i  9589  enfin1ai  9652  isfin5-2  9659  fin1a2lem7  9674  fin1a2lem11  9678  fin1a2lem13  9680  axdc3lem2  9719  engch  9896  eltskg  10018  tsken  10022  ltsonq  10237  addcanpr  10314  ltsosr  10362  axpre-lttri  10433  lemul1  11340  mulge0b  11358  mulle0b  11359  mulsuble0b  11360  nn1m1nn  11506  avgle  11727  nn0sub  11795  elznn0  11844  elz2  11847  nneo  11915  uztric  12115  mul2lt0bi  12345  ltxr  12360  xrrebnd  12411  xmulval  12468  xmulneg1  12512  ixxun  12604  iccsplit  12721  fzsplit2  12782  uzsplit  12829  nelfzo  12893  fzospliti  12919  fzouzsplit  12922  sqeqor  13428  swrdnd  13852  sumeq1  14879  sumeq2w  14882  sumeq2ii  14883  fz1f1o  14900  summo  14907  fsum  14910  prodeq1f  15095  prodeq2w  15099  prodeq2ii  15100  prodmo  15123  fprod  15128  ruclem12  15427  odd2np1lem  15522  dvdsprime  15860  coprm  15884  vdwapun  16139  vdwlem6  16151  vdwlem10  16155  mreexexlemd  16744  mreexexd  16748  istos  17474  tosso  17475  tsrlin  17658  tsrss  17662  isdomn  19756  prmirredlem  20322  domnchr  20361  zntoslem  20385  znfld  20389  fctop  21296  cctop  21298  ppttop  21299  pptbas  21300  isufil  22195  ufilss  22197  fixufil  22214  fin1aufil  22224  xpsdsval  22674  nlmmul0or  22975  pmltpclem1  23732  iundisj2  23833  mbfmax  23933  dvne0  24291  fta1glem2  24443  plymul0or  24553  ofmulrt  24554  quotval  24564  plydivlem3  24567  plydivlem4  24568  plydivex  24569  plydivalg  24571  quotlem  24572  aalioulem2  24605  quad2  25098  dcubic2  25103  dcubic  25105  dquartlem1  25110  dquart  25112  quart  25120  leibpilem2  25201  wilthlem1  25327  muval2  25393  perfectlem2  25488  lgslem1  25555  pntpbnd1  25844  legtrid  26059  legso  26067  ishlg  26070  lnhl  26083  symquadlem  26157  islmib  26255  isinag  26307  isinagd  26308  inaghl  26314  brbtwn2  26374  axcontlem2  26434  axcontlem4  26436  axcontlem11  26443  edglnl  26611  nb3grprlem2  26846  hashecclwwlkn1  27543  nfrgr2v  27743  h1datom  29050  atss  29814  atom1d  29821  atord  29856  chirred  29863  elimifd  29987  disji2f  30017  disjif2  30021  disjxpin  30028  iundisj2f  30030  disjunsn  30034  brprop  30121  fzsplit3  30203  iundisj2fi  30206  f1ocnt  30209  resstos  30321  tleile  30322  trleile  30327  smatrcl  30676  fsumcvg4  30810  erdsze2lem2  32060  satf  32209  satfv1  32219  satfbrsuc  32222  satfrnmapom  32226  satf0op  32233  sat1el2xp  32235  fmlafvel  32241  fmlasuc  32242  fmla1  32243  isfmlasuc  32244  fmlaomn0  32246  fmlasucdisj  32255  satffunlem1lem1  32258  satffunlem1lem2  32259  satffunlem2lem1  32260  dmopab3rexdif  32261  satffunlem2lem2  32262  satfv1fvfmla1  32279  2goelgoanfmla1  32280  satefvfmla1  32281  eqfunresadj  32613  funpsstri  32617  soseq  32706  seglelin  33187  lineunray  33218  topdifinffinlem  34178  topdifinffin  34179  topdifinfeq  34181  mblfinlem2  34480  itg2addnclem2  34494  iblabsnclem  34505  ftc1anclem5  34521  fdc1  34572  unichnidl  34860  ispridl  34863  maxidlmax  34872  qsdisjALTV  35400  lcvexchlem4  35723  lcvexchlem5  35724  2at0mat0  36211  pmapjoin  36538  cdlemg17h  37354  dihlspsnat  38019  lzunuz  38869  dvdsrabdioph  38911  acongeq12d  39080  jm2.25  39100  rmydioph  39115  expdioph  39124  fnwe2val  39153  aomclem8  39165  brfvrcld2  39541  uneqsn  39877  ntrneixb  39949  ntrneix3  39951  ntrneix13  39953  unima  40981  disjinfi  41013  salexct  42179  salexct2  42184  salexct3  42187  salgencntex  42188  salgensscntex  42189  nnfoctbdjlem  42299  nnfoctbdj  42300  iundjiun  42304  opprb  42802  euoreqb  42844  el1fzopredsuc  43061  iccpartgel  43091  paireqne  43175  divgcdoddALTV  43349  perfectALTVlem2  43389  lindslinindsimp2lem5  44017  ldepspr  44028  rrx2pnedifcoorneor  44204  rrx2plord  44208  rrx2plordisom  44211  itsclc0yqsol  44252