Theorem orbi12d 715

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
bi12d.1	|- ( ph -> ( ps <-> ch ) )
bi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
orbi12d	|- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	orbi1d 708	. 2 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
3		bi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	orbi2d 707	. 2 |- ( ph -> ( ( ch \/ th ) <-> ( ch \/ ta ) ) )
5	2, 4	bitrd 257	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  pm4.39  880  3orbi123d  1335  cadbi123d  1509  eueq3  3247  sbcor  3344  unjust  3441  elun  3607  elprg  4013  eltpg  4040  rabsnifsb  4066  rabrsn  4068  preq12bg  4177  disji2  4408  disjprg  4417  disjxun  4419  opthneg  4698  swopolem  4781  sotrieq  4799  isso2i  4804  somin1  5250  fununi  5665  unpreima  6019  ordsucun  6664  funcnvuni  6758  fun11iun  6765  frxp  6915  xporderlem  6916  poxp  6917  fnwelem  6920  fnse  6922  oacan  7255  omword  7277  oeword  7297  oeoa  7304  qsdisj  7446  wemapso2lem  8071  brwdom  8086  cantnflem1  8197  r0weon  8446  infxpen  8448  sornom  8709  fin1ai  8725  isfin5  8731  isfin6  8732  sdom2en01  8734  enfin2i  8753  enfin1ai  8816  isfin5-2  8823  fin1a2lem7  8838  fin1a2lem11  8842  fin1a2lem13  8844  axdc3lem2  8883  engch  9055  eltskg  9177  tsken  9181  ltsonq  9396  addcanpr  9473  ltsosr  9520  axpre-lttri  9591  lemul1  10459  mulge0b  10477  mulle0b  10478  mulsuble0b  10479  nn1m1nn  10631  avgle  10856  nn0sub  10922  elznn0  10954  elz2  10956  nneo  11021  uztric  11182  mul2lt0bi  11404  ltxr  11417  xrrebnd  11465  xmulval  11520  xmulneg1  11557  ixxun  11653  iccsplit  11767  fzsplit2  11826  uzsplit  11868  nelfzo  11927  fzospliti  11952  fzouzsplit  11955  sqeqor  12389  swrdnd  12784  sumeq1  13748  sumeq2w  13751  sumeq2ii  13752  fz1f1o  13769  summo  13776  fsum  13779  prodeq1f  13955  prodeq2w  13959  prodeq2ii  13960  prodmo  13983  fprod  13988  ruclem12  14286  odd2np1lem  14357  dvdsprime  14630  coprm  14650  vdwapun  14917  vdwlem6  14929  vdwlem10  14933  mreexexlemd  15543  mreexexd  15547  istos  16274  tosso  16275  tsrlin  16458  tsrss  16462  isdomn  18511  prmirredlem  19056  domnchr  19095  zntoslem  19119  znfld  19123  fctop  20011  cctop  20013  ppttop  20014  pptbas  20015  isufil  20910  ufilss  20912  fixufil  20929  fin1aufil  20939  xpsdsval  21388  nlmmul0or  21678  pmltpclem1  22391  iundisj2  22494  mbfmax  22597  dvne0  22955  fta1glem2  23109  plymul0or  23226  ofmulrt  23227  quotval  23237  plydivlem3  23240  plydivlem4  23241  plydivex  23242  plydivalg  23244  quotlem  23245  aalioulem2  23281  quad2  23757  dcubic2  23762  dcubic  23764  dquartlem1  23769  dquart  23771  quart  23779  leibpilem2  23859  wilthlem1  23985  muval2  24053  perfectlem2  24150  lgslem1  24216  pntpbnd1  24416  legtrid  24628  legso  24636  ishlg  24639  lnhl  24652  symquadlem  24726  islmib  24821  isinag  24871  inaghl  24873  brbtwn2  24927  axcontlem2  24987  axcontlem4  24989  axcontlem11  24996  nb3graprlem2  25172  hashecclwwlkn1  25554  frgra2v  25719  h1datom  27227  atss  27991  atom1d  27998  atord  28033  chirred  28040  elimifd  28156  disji2f  28183  disjif2  28187  disjxpin  28194  iundisj2f  28196  disjunsn  28200  fzsplit3  28370  iundisj2fi  28373  f1ocnt  28376  resstos  28422  tleile  28423  trleile  28428  smatrcl  28624  fsumcvg4  28758  erdsze2lem2  29929  funpsstri  30407  soseq  30493  seglelin  30882  lineunray  30913  topdifinffinlem  31708  topdifinffin  31709  topdifinfeq  31711  mblfinlem2  31936  itg2addnclem2  31952  iblabsnclem  31963  ftc1anclem5  31979  fdc1  32033  unichnidl  32222  ispridl  32225  maxidlmax  32234  lcvexchlem4  32566  lcvexchlem5  32567  2at0mat0  33053  pmapjoin  33380  cdlemg17h  34198  dihlspsnat  34864  lzunuz  35573  dvdsrabdioph  35616  acongeq12d  35793  jm2.25  35818  rmydioph  35833  expdioph  35842  fnwe2val  35871  aomclem8  35883  brfvrcld2  36188  sbcorgOLD  36793  unima  37322  disjinfi  37362  nnfoctbdjlem  38116  nnfoctbdj  38117  iundjiun  38121  el1fzopredsuc  38478  iccpartgel  38499  divgcdoddALTV  38567  perfectALTVlem2  38600  lindslinindsimp2lem5  39599  ldepspr  39610