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  866  3orbi123d  1288  cadbi123d  1424  eueq3  3129  sbcor  3226  sbcorgOLD  3227  unjust  3327  elun  3492  elprg  3888  eltpg  3913  rabsnifsb  3938  rabrsn  3940  preq12bg  4046  disji2  4274  disjprg  4283  disjxun  4285  opthneg  4566  swopolem  4645  sotrieq  4663  isso2i  4668  somin1  5229  fununi  5479  unpreima  5824  ordsucun  6431  funcnvuni  6525  fun11iun  6532  frxp  6677  xporderlem  6678  poxp  6679  fnwelem  6682  fnse  6684  oacan  6979  omword  7001  oeword  7021  oeoa  7028  qsdisj  7169  wemapso2OLD  7758  wemapso2lem  7759  brwdom  7774  cantnflem1  7889  cantnflem1OLD  7912  r0weon  8171  infxpen  8173  sornom  8438  fin1ai  8454  isfin5  8460  isfin6  8461  sdom2en01  8463  enfin2i  8482  enfin1ai  8545  isfin5-2  8552  fin1a2lem7  8567  fin1a2lem11  8571  fin1a2lem13  8573  axdc3lem2  8612  engch  8787  eltskg  8909  tsken  8913  ltsonq  9130  addcanpr  9207  ltsosr  9253  axpre-lttri  9324  lemul1  10173  mulge0b  10191  mulle0b  10192  mulsuble0b  10193  nn1m1nn  10334  avgle  10558  nn0sub  10622  elznn0  10653  elz2  10655  nneo  10717  uztric  10874  ltxr  11087  xrrebnd  11132  xmulval  11187  xmulneg1  11224  ixxun  11308  iccsplit  11410  fzsplit2  11466  uzsplit  11522  fzospliti  11573  fzouzsplit  11576  sqeqor  11972  sumeq1  13158  sumeq2w  13161  sumeq2ii  13162  fz1f1o  13179  summo  13186  fsum  13189  ruclem12  13515  odd2np1lem  13583  dvdsprime  13768  coprm  13778  vdwapun  14027  vdwlem6  14039  vdwlem10  14043  mreexexlemd  14574  mreexexd  14578  istos  15197  tosso  15198  tsrlin  15381  tsrss  15385  isdomn  17343  prmirredlem  17892  prmirredlemOLD  17895  domnchr  17938  zntoslem  17964  znfld  17968  fctop  18583  cctop  18585  ppttop  18586  pptbas  18587  isufil  19451  ufilss  19453  fixufil  19470  fin1aufil  19480  xpsdsval  19931  nlmmul0or  20239  pmltpclem1  20907  iundisj2  21005  mbfmax  21102  dvne0  21458  fta1glem2  21613  plymul0or  21722  ofmulrt  21723  quotval  21733  plydivlem3  21736  plydivlem4  21737  plydivex  21738  plydivalg  21740  quotlem  21741  aalioulem2  21774  quad2  22209  dcubic2  22214  dcubic  22216  dquartlem1  22221  dquart  22223  quart  22231  leibpilem2  22311  wilthlem1  22381  muval2  22447  perfectlem2  22544  lgslem1  22610  pntpbnd1  22810  legtrid  22993  symquadlem  23048  brbtwn2  23102  axcontlem2  23162  axcontlem4  23164  axcontlem11  23171  nb3graprlem2  23311  h1datom  24936  atss  25701  atom1d  25708  atord  25743  chirred  25750  elimifd  25856  disji2f  25872  disjif2  25876  disjxpin  25881  iundisj2f  25883  disjunsn  25887  mul2lt0bi  25993  fzsplit3  26029  iundisj2fi  26032  resstos  26072  tleile  26073  trleile  26078  fsumcvg4  26332  erdsze2lem2  27044  prodeq1f  27372  prodeq2w  27376  prodeq2ii  27377  prodmo  27400  fprod  27405  funpsstri  27527  soseq  27666  seglelin  28098  lineunray  28129  mblfinlem2  28382  itg2addnclem2  28397  iblabsnclem  28408  ftc1anclem5  28424  fdc1  28595  unichnidl  28784  ispridl  28787  maxidlmax  28796  lzunuz  29059  dvdsrabdioph  29101  acongeq12d  29275  jm2.25  29301  rmydioph  29316  expdioph  29325  fnwe2val  29355  aomclem8  29367  hashecclwwlkn1  30461  frgra2v  30544  lindslinindsimp2lem5  30885  ldepspr  30896  lcvexchlem4  32522  lcvexchlem5  32523  2at0mat0  33009  pmapjoin  33336  cdlemg17h  34152  dihlspsnat  34818