Theorem orbi12d 709

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 702	. 2 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
3		bi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	orbi2d 701	. 2 |- ( ph -> ( ( ch \/ th ) <-> ( ch \/ ta ) ) )
5	2, 4	bitrd 253	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  pm4.39  871  3orbi123d  1299  cadbi123d  1438  eueq3  3260  sbcor  3358  sbcorgOLD  3359  unjust  3465  elun  3630  elprg  4030  eltpg  4056  rabsnifsb  4083  rabrsn  4085  preq12bg  4194  disji2  4424  disjprg  4433  disjxun  4435  opthneg  4716  swopolem  4799  sotrieq  4817  isso2i  4822  somin1  5393  fununi  5644  unpreima  5998  ordsucun  6645  funcnvuni  6738  fun11iun  6745  frxp  6895  xporderlem  6896  poxp  6897  fnwelem  6900  fnse  6902  oacan  7199  omword  7221  oeword  7241  oeoa  7248  qsdisj  7390  wemapso2OLD  7980  wemapso2lem  7981  brwdom  7996  cantnflem1  8111  cantnflem1OLD  8134  r0weon  8393  infxpen  8395  sornom  8660  fin1ai  8676  isfin5  8682  isfin6  8683  sdom2en01  8685  enfin2i  8704  enfin1ai  8767  isfin5-2  8774  fin1a2lem7  8789  fin1a2lem11  8793  fin1a2lem13  8795  axdc3lem2  8834  engch  9009  eltskg  9131  tsken  9135  ltsonq  9350  addcanpr  9427  ltsosr  9474  axpre-lttri  9545  lemul1  10401  mulge0b  10419  mulle0b  10420  mulsuble0b  10421  nn1m1nn  10563  avgle  10787  nn0sub  10853  elznn0  10886  elz2  10888  nneo  10953  uztric  11113  ltxr  11335  xrrebnd  11380  xmulval  11435  xmulneg1  11472  ixxun  11556  iccsplit  11664  fzsplit2  11721  uzsplit  11761  fzospliti  11839  fzouzsplit  11842  sqeqor  12264  sumeq1  13493  sumeq2w  13496  sumeq2ii  13497  fz1f1o  13514  summo  13521  fsum  13524  prodeq1f  13697  prodeq2w  13701  prodeq2ii  13702  prodmo  13725  fprod  13730  ruclem12  13956  odd2np1lem  14027  dvdsprime  14212  coprm  14223  vdwapun  14474  vdwlem6  14486  vdwlem10  14490  mreexexlemd  15023  mreexexd  15027  istos  15644  tosso  15645  tsrlin  15828  tsrss  15832  isdomn  17922  prmirredlem  18501  prmirredlemOLD  18504  domnchr  18547  zntoslem  18573  znfld  18577  fctop  19483  cctop  19485  ppttop  19486  pptbas  19487  isufil  20382  ufilss  20384  fixufil  20401  fin1aufil  20411  xpsdsval  20862  nlmmul0or  21170  pmltpclem1  21838  iundisj2  21937  mbfmax  22034  dvne0  22390  fta1glem2  22545  plymul0or  22655  ofmulrt  22656  quotval  22666  plydivlem3  22669  plydivlem4  22670  plydivex  22671  plydivalg  22673  quotlem  22674  aalioulem2  22707  quad2  23148  dcubic2  23153  dcubic  23155  dquartlem1  23160  dquart  23162  quart  23170  leibpilem2  23250  wilthlem1  23320  muval2  23386  perfectlem2  23483  lgslem1  23549  pntpbnd1  23749  legtrid  23956  legso  23963  ishlg  23964  symquadlem  24044  islmib  24131  brbtwn2  24186  axcontlem2  24246  axcontlem4  24248  axcontlem11  24255  nb3graprlem2  24430  hashecclwwlkn1  24812  frgra2v  24977  h1datom  26478  atss  27243  atom1d  27250  atord  27285  chirred  27292  elimifd  27399  disji2f  27416  disjif2  27420  disjxpin  27425  iundisj2f  27427  disjunsn  27431  mul2lt0bi  27547  fzsplit3  27577  iundisj2fi  27580  resstos  27626  tleile  27627  trleile  27632  fsumcvg4  27910  erdsze2lem2  28626  funpsstri  29171  soseq  29310  seglelin  29742  lineunray  29773  mblfinlem2  30028  itg2addnclem2  30043  iblabsnclem  30054  ftc1anclem5  30070  fdc1  30215  unichnidl  30404  ispridl  30407  maxidlmax  30416  lzunuz  30677  dvdsrabdioph  30719  acongeq12d  30893  jm2.25  30917  rmydioph  30932  expdioph  30941  fnwe2val  30971  aomclem8  30983  unima  31395  lindslinindsimp2lem5  32933  ldepspr  32944  lcvexchlem4  34637  lcvexchlem5  34638  2at0mat0  35124  pmapjoin  35451  cdlemg17h  36269  dihlspsnat  36935