Theorem orbi12d 707

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

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

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 368

This theorem is referenced by:  pm4.39  869  3orbi123d  1296  cadbi123d  1458  eueq3  3212  sbcor  3309  unjust  3406  elun  3572  elprg  3973  eltpg  3999  rabsnifsb  4025  rabrsn  4027  preq12bg  4136  disji2  4367  disjprg  4376  disjxun  4378  opthneg  4654  swopolem  4736  sotrieq  4754  isso2i  4759  somin1  5326  fununi  5575  unpreima  5928  ordsucun  6577  funcnvuni  6670  fun11iun  6677  frxp  6827  xporderlem  6828  poxp  6829  fnwelem  6832  fnse  6834  oacan  7133  omword  7155  oeword  7175  oeoa  7182  qsdisj  7324  wemapso2OLD  7910  wemapso2lem  7911  brwdom  7926  cantnflem1  8039  cantnflem1OLD  8062  r0weon  8321  infxpen  8323  sornom  8588  fin1ai  8604  isfin5  8610  isfin6  8611  sdom2en01  8613  enfin2i  8632  enfin1ai  8695  isfin5-2  8702  fin1a2lem7  8717  fin1a2lem11  8721  fin1a2lem13  8723  axdc3lem2  8762  engch  8935  eltskg  9057  tsken  9061  ltsonq  9276  addcanpr  9353  ltsosr  9400  axpre-lttri  9471  lemul1  10329  mulge0b  10347  mulle0b  10348  mulsuble0b  10349  nn1m1nn  10490  avgle  10715  nn0sub  10781  elznn0  10814  elz2  10816  nneo  10881  uztric  11040  ltxr  11263  xrrebnd  11308  xmulval  11363  xmulneg1  11400  ixxun  11484  iccsplit  11592  fzsplit2  11649  uzsplit  11690  nelfzo  11745  fzospliti  11770  fzouzsplit  11773  sqeqor  12203  swrdnd  12587  sumeq1  13532  sumeq2w  13535  sumeq2ii  13536  fz1f1o  13553  summo  13560  fsum  13563  prodeq1f  13736  prodeq2w  13740  prodeq2ii  13741  prodmo  13764  fprod  13769  ruclem12  13995  odd2np1lem  14066  dvdsprime  14251  coprm  14262  vdwapun  14513  vdwlem6  14525  vdwlem10  14529  mreexexlemd  15070  mreexexd  15074  istos  15801  tosso  15802  tsrlin  15985  tsrss  15989  isdomn  18075  prmirredlem  18642  domnchr  18681  zntoslem  18705  znfld  18709  fctop  19609  cctop  19611  ppttop  19612  pptbas  19613  isufil  20508  ufilss  20510  fixufil  20527  fin1aufil  20537  xpsdsval  20988  nlmmul0or  21296  pmltpclem1  21964  iundisj2  22063  mbfmax  22160  dvne0  22516  fta1glem2  22671  plymul0or  22781  ofmulrt  22782  quotval  22792  plydivlem3  22795  plydivlem4  22796  plydivex  22797  plydivalg  22799  quotlem  22800  aalioulem2  22833  quad2  23305  dcubic2  23310  dcubic  23312  dquartlem1  23317  dquart  23319  quart  23327  leibpilem2  23407  wilthlem1  23478  muval2  23544  perfectlem2  23641  lgslem1  23707  pntpbnd1  23907  legtrid  24119  legso  24126  ishlg  24127  symquadlem  24207  islmib  24294  brbtwn2  24350  axcontlem2  24410  axcontlem4  24412  axcontlem11  24419  nb3graprlem2  24594  hashecclwwlkn1  24976  frgra2v  25141  h1datom  26638  atss  27402  atom1d  27409  atord  27444  chirred  27451  elimifd  27569  disji2f  27596  disjif2  27600  disjxpin  27607  iundisj2f  27609  disjunsn  27613  mul2lt0bi  27749  fzsplit3  27782  iundisj2fi  27785  resstos  27831  tleile  27832  trleile  27837  fsumcvg4  28117  erdsze2lem2  28873  funpsstri  29397  soseq  29535  seglelin  29955  lineunray  29986  mblfinlem2  30253  itg2addnclem2  30269  iblabsnclem  30280  ftc1anclem5  30296  fdc1  30441  unichnidl  30630  ispridl  30633  maxidlmax  30642  lzunuz  30902  dvdsrabdioph  30945  acongeq12d  31118  jm2.25  31143  rmydioph  31158  expdioph  31167  fnwe2val  31197  aomclem8  31209  unima  31643  divgcdoddALTV  32559  perfectALTVlem2  32579  lindslinindsimp2lem5  33298  ldepspr  33309  sbcorgOLD  33672  lcvexchlem4  35210  lcvexchlem5  35211  2at0mat0  35697  pmapjoin  36024  cdlemg17h  36842  dihlspsnat  37508