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  869  3orbi123d  1298  cadbi123d  1434  eueq3  3278  sbcor  3376  sbcorgOLD  3377  unjust  3480  elun  3645  elprg  4043  eltpg  4069  rabsnifsb  4095  rabrsn  4097  preq12bg  4205  disji2  4434  disjprg  4443  disjxun  4445  opthneg  4726  swopolem  4809  sotrieq  4827  isso2i  4832  somin1  5402  fununi  5653  unpreima  6006  ordsucun  6639  funcnvuni  6737  fun11iun  6744  frxp  6893  xporderlem  6894  poxp  6895  fnwelem  6898  fnse  6900  oacan  7197  omword  7219  oeword  7239  oeoa  7246  qsdisj  7388  wemapso2OLD  7976  wemapso2lem  7977  brwdom  7992  cantnflem1  8107  cantnflem1OLD  8130  r0weon  8389  infxpen  8391  sornom  8656  fin1ai  8672  isfin5  8678  isfin6  8679  sdom2en01  8681  enfin2i  8700  enfin1ai  8763  isfin5-2  8770  fin1a2lem7  8785  fin1a2lem11  8789  fin1a2lem13  8791  axdc3lem2  8830  engch  9005  eltskg  9127  tsken  9131  ltsonq  9346  addcanpr  9423  ltsosr  9470  axpre-lttri  9541  lemul1  10393  mulge0b  10411  mulle0b  10412  mulsuble0b  10413  nn1m1nn  10555  avgle  10779  nn0sub  10845  elznn0  10878  elz2  10880  nneo  10943  uztric  11102  ltxr  11323  xrrebnd  11368  xmulval  11423  xmulneg1  11460  ixxun  11544  iccsplit  11652  fzsplit2  11709  uzsplit  11749  fzospliti  11824  fzouzsplit  11827  sqeqor  12249  sumeq1  13473  sumeq2w  13476  sumeq2ii  13477  fz1f1o  13494  summo  13501  fsum  13504  ruclem12  13834  odd2np1lem  13903  dvdsprime  14088  coprm  14099  vdwapun  14350  vdwlem6  14362  vdwlem10  14366  mreexexlemd  14898  mreexexd  14902  istos  15521  tosso  15522  tsrlin  15705  tsrss  15709  isdomn  17730  prmirredlem  18306  prmirredlemOLD  18309  domnchr  18352  zntoslem  18378  znfld  18382  fctop  19287  cctop  19289  ppttop  19290  pptbas  19291  isufil  20155  ufilss  20157  fixufil  20174  fin1aufil  20184  xpsdsval  20635  nlmmul0or  20943  pmltpclem1  21611  iundisj2  21710  mbfmax  21807  dvne0  22163  fta1glem2  22318  plymul0or  22427  ofmulrt  22428  quotval  22438  plydivlem3  22441  plydivlem4  22442  plydivex  22443  plydivalg  22445  quotlem  22446  aalioulem2  22479  quad2  22914  dcubic2  22919  dcubic  22921  dquartlem1  22926  dquart  22928  quart  22936  leibpilem2  23016  wilthlem1  23086  muval2  23152  perfectlem2  23249  lgslem1  23315  pntpbnd1  23515  legtrid  23721  legso  23728  symquadlem  23790  islmib  23846  brbtwn2  23900  axcontlem2  23960  axcontlem4  23962  axcontlem11  23969  nb3graprlem2  24144  hashecclwwlkn1  24526  frgra2v  24691  h1datom  26192  atss  26957  atom1d  26964  atord  26999  chirred  27006  elimifd  27111  disji2f  27127  disjif2  27131  disjxpin  27136  iundisj2f  27138  disjunsn  27142  mul2lt0bi  27253  fzsplit3  27283  iundisj2fi  27286  resstos  27326  tleile  27327  trleile  27332  fsumcvg4  27584  erdsze2lem2  28304  prodeq1f  28633  prodeq2w  28637  prodeq2ii  28638  prodmo  28661  fprod  28666  funpsstri  28788  soseq  28927  seglelin  29359  lineunray  29390  mblfinlem2  29645  itg2addnclem2  29660  iblabsnclem  29671  ftc1anclem5  29687  fdc1  29858  unichnidl  30047  ispridl  30050  maxidlmax  30059  lzunuz  30321  dvdsrabdioph  30363  acongeq12d  30537  jm2.25  30561  rmydioph  30576  expdioph  30585  fnwe2val  30615  aomclem8  30627  unima  31035  lindslinindsimp2lem5  32153  ldepspr  32164  lcvexchlem4  33843  lcvexchlem5  33844  2at0mat0  34330  pmapjoin  34657  cdlemg17h  35473  dihlspsnat  36139