Theorem orbi12d 919

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 847

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 210  df-or 848

This theorem is referenced by:  pm4.39  977  ifpbi123d  1080  ifpbi123dOLD  1081  3orbi123d  1437  cadbi123d  1617  eueq3  3624  sbcor  3747  unjust  3870  elun  4063  elprg  4562  eltpg  4601  reuprg0  4618  rabsnifsb  4638  rabrsn  4640  preq12bg  4764  uniprg  4836  disji2  5035  disjprgw  5048  disjprg  5049  disjxun  5051  swopolem  5478  sotrieq  5497  isso2i  5503  dmopab2rex  5786  somin1  5998  ordequn  6313  fununi  6455  unima  6786  unpreima  6883  ordsucun  7604  funcnvuni  7709  fiunlem  7715  frxp  7893  xporderlem  7894  poxp  7895  fnwelem  7898  fnse  7900  oacan  8276  omword  8298  oeword  8318  oeoa  8325  qsdisj  8476  wemapso2lem  9168  brwdom  9183  cantnflem1  9304  r0weon  9626  infxpen  9628  sornom  9891  fin1ai  9907  isfin5  9913  isfin6  9914  sdom2en01  9916  enfin2i  9935  enfin1ai  9998  isfin5-2  10005  fin1a2lem7  10020  fin1a2lem11  10024  fin1a2lem13  10026  axdc3lem2  10065  engch  10242  eltskg  10364  tsken  10368  ltsonq  10583  addcanpr  10660  ltsosr  10708  axpre-lttri  10779  lemul1  11684  mulge0b  11702  mulle0b  11703  mulsuble0b  11704  nn1m1nn  11851  avgle  12072  nn0sub  12140  elznn0  12191  elz2  12194  nneo  12261  uztric  12462  mul2lt0bi  12692  ltxr  12707  xrrebnd  12758  xmulval  12815  xmulneg1  12859  ixxun  12951  iccsplit  13073  fzsplit2  13137  uzsplit  13184  nelfzo  13248  fzospliti  13274  fzouzsplit  13277  sqeqor  13784  swrdnd  14219  sumeq1  15252  sumeq2w  15256  sumeq2ii  15257  fz1f1o  15274  summo  15281  fsum  15284  prodeq1f  15470  prodeq2w  15474  prodeq2ii  15475  prodmo  15498  fprod  15503  ruclem12  15802  odd2np1lem  15901  dvdsprime  16244  coprm  16268  vdwapun  16527  vdwlem6  16539  vdwlem10  16543  mreexexlemd  17147  mreexexd  17151  istos  17924  tosso  17925  tleile  17927  tsrlin  18091  tsrss  18095  isdomn  20332  prmirredlem  20459  domnchr  20497  zntoslem  20521  znfld  20525  fctop  21901  cctop  21903  ppttop  21904  pptbas  21905  isufil  22800  ufilss  22802  fixufil  22819  fin1aufil  22829  xpsdsval  23279  nlmmul0or  23581  pmltpclem1  24345  iundisj2  24446  mbfmax  24546  dvne0  24908  fta1glem2  25064  plymul0or  25174  ofmulrt  25175  quotval  25185  plydivlem3  25188  plydivlem4  25189  plydivex  25190  plydivalg  25192  quotlem  25193  aalioulem2  25226  quad2  25722  dcubic2  25727  dcubic  25729  dquartlem1  25734  dquart  25736  quart  25744  leibpilem2  25824  wilthlem1  25950  muval2  26016  perfectlem2  26111  lgslem1  26178  pntpbnd1  26467  legtrid  26682  legso  26690  ishlg  26693  lnhl  26706  symquadlem  26780  islmib  26878  isinag  26929  isinagd  26930  inaghl  26936  brbtwn2  26996  axcontlem2  27056  axcontlem4  27058  axcontlem11  27065  edglnl  27234  nb3grprlem2  27469  hashecclwwlkn1  28160  nfrgr2v  28355  h1datom  29663  atss  30427  atom1d  30434  atord  30469  chirred  30476  elimifd  30605  disji2f  30635  disjif2  30639  disjxpin  30646  iundisj2f  30648  disjunsn  30652  brprop  30750  fzsplit3  30835  iundisj2fi  30838  f1ocnt  30843  resstos  30964  trleile  30968  isprmidl  31327  prmidlc  31338  qsidomlem1  31342  qsidomlem2  31343  mxidlmax  31351  rprmval  31378  isrprm  31379  smatrcl  31460  fsumcvg4  31614  erdsze2lem2  32879  satf  33028  satfv1  33038  satfbrsuc  33041  satfrnmapom  33045  satf0op  33052  sat1el2xp  33054  fmlafvel  33060  fmlasuc  33061  fmla1  33062  isfmlasuc  33063  fmlaomn0  33065  fmlasucdisj  33074  satffunlem1lem1  33077  satffunlem1lem2  33078  satffunlem2lem1  33079  dmopab3rexdif  33080  satffunlem2lem2  33081  satfv1fvfmla1  33098  2goelgoanfmla1  33099  satefvfmla1  33100  eqfunresadj  33454  funpsstri  33458  xpord2lem  33526  poxp2  33527  xpord3lem  33532  poxp3  33533  soseq  33540  seglelin  34155  lineunray  34186  topdifinffinlem  35255  topdifinffin  35256  topdifinfeq  35258  mblfinlem2  35552  itg2addnclem2  35566  iblabsnclem  35577  ftc1anclem5  35591  fdc1  35641  unichnidl  35926  ispridl  35929  maxidlmax  35938  qsdisjALTV  36465  lcvexchlem4  36788  lcvexchlem5  36789  2at0mat0  37276  pmapjoin  37603  cdlemg17h  38419  dihlspsnat  39084  lzunuz  40293  dvdsrabdioph  40335  acongeq12d  40504  jm2.25  40524  rmydioph  40539  expdioph  40548  fnwe2val  40577  aomclem8  40589  sqrtcvallem1  40915  brfvrcld2  40977  uneqsn  41310  ntrneixb  41382  ntrneix3  41384  ntrneix13  41386  mnringmulrcld  41519  disjinfi  42404  salexct  43548  salexct2  43553  salexct3  43556  salgencntex  43557  salgensscntex  43558  nnfoctbdjlem  43668  nnfoctbdj  43669  iundjiun  43673  opprb  44197  euoreqb  44273  el1fzopredsuc  44490  iccpartgel  44554  paireqne  44636  divgcdoddALTV  44807  perfectALTVlem2  44847  lindslinindsimp2lem5  45476  ldepspr  45487  rrx2pnedifcoorneor  45735  rrx2plord  45739  rrx2plordisom  45742  itsclc0yqsol  45783