Theorem orbi12d 746

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

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  pm4.39  915  ifpbi123d  1027  3orbi123d  1398  cadbi123d  1549  eueq3  3381  sbcor  3479  unjust  3578  elun  3753  elprg  4196  eltpg  4227  rabsnifsb  4257  rabrsn  4259  preq12bg  4386  disji2  4636  disjprg  4648  disjxun  4651  swopolem  5044  sotrieq  5062  isso2i  5067  somin1  5529  ordequn  5828  fununi  5964  unpreima  6341  ordsucun  7025  funcnvuni  7119  fun11iun  7126  frxp  7287  xporderlem  7288  poxp  7289  fnwelem  7292  fnse  7294  oacan  7628  omword  7650  oeword  7670  oeoa  7677  qsdisj  7824  wemapso2lem  8457  brwdom  8472  cantnflem1  8586  r0weon  8835  infxpen  8837  sornom  9099  fin1ai  9115  isfin5  9121  isfin6  9122  sdom2en01  9124  enfin2i  9143  enfin1ai  9206  isfin5-2  9213  fin1a2lem7  9228  fin1a2lem11  9232  fin1a2lem13  9234  axdc3lem2  9273  engch  9450  eltskg  9572  tsken  9576  ltsonq  9791  addcanpr  9868  ltsosr  9915  axpre-lttri  9986  lemul1  10875  mulge0b  10893  mulle0b  10894  mulsuble0b  10895  nn1m1nn  11040  avgle  11274  nn0sub  11343  elznn0  11392  elz2  11394  nneo  11461  uztric  11709  mul2lt0bi  11936  ltxr  11949  xrrebnd  11999  xmulval  12056  xmulneg1  12099  ixxun  12191  iccsplit  12305  fzsplit2  12366  uzsplit  12412  nelfzo  12475  fzospliti  12500  fzouzsplit  12503  sqeqor  12978  swrdnd  13432  sumeq1  14419  sumeq2w  14422  sumeq2ii  14423  fz1f1o  14441  summo  14448  fsum  14451  prodeq1f  14638  prodeq2w  14642  prodeq2ii  14643  prodmo  14666  fprod  14671  ruclem12  14970  odd2np1lem  15064  dvdsprime  15400  coprm  15423  vdwapun  15678  vdwlem6  15690  vdwlem10  15694  mreexexlemd  16304  mreexexd  16308  mreexexdOLD  16309  istos  17035  tosso  17036  tsrlin  17219  tsrss  17223  isdomn  19294  prmirredlem  19841  domnchr  19880  zntoslem  19905  znfld  19909  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  isufil  21707  ufilss  21709  fixufil  21726  fin1aufil  21736  xpsdsval  22186  nlmmul0or  22487  pmltpclem1  23217  iundisj2  23317  mbfmax  23416  dvne0  23774  fta1glem2  23926  plymul0or  24036  ofmulrt  24037  quotval  24047  plydivlem3  24050  plydivlem4  24051  plydivex  24052  plydivalg  24054  quotlem  24055  aalioulem2  24088  quad2  24566  dcubic2  24571  dcubic  24573  dquartlem1  24578  dquart  24580  quart  24588  leibpilem2  24668  wilthlem1  24794  muval2  24860  perfectlem2  24955  lgslem1  25022  pntpbnd1  25275  legtrid  25486  legso  25494  ishlg  25497  lnhl  25510  symquadlem  25584  islmib  25679  isinag  25729  inaghl  25731  brbtwn2  25785  axcontlem2  25845  axcontlem4  25847  axcontlem11  25854  edglnl  26038  nb3grprlem2  26283  hashecclwwlksn1  26954  nfrgr2v  27136  h1datom  28441  atss  29205  atom1d  29212  atord  29247  chirred  29254  elimifd  29362  disji2f  29390  disjif2  29394  disjxpin  29401  iundisj2f  29403  disjunsn  29407  fzsplit3  29553  iundisj2fi  29556  f1ocnt  29559  resstos  29660  tleile  29661  trleile  29666  smatrcl  29862  fsumcvg4  29996  erdsze2lem2  31186  eqfunresadj  31659  funpsstri  31663  soseq  31751  seglelin  32223  lineunray  32254  topdifinffinlem  33195  topdifinffin  33196  topdifinfeq  33198  mblfinlem2  33447  itg2addnclem2  33462  iblabsnclem  33473  ftc1anclem5  33489  fdc1  33542  unichnidl  33830  ispridl  33833  maxidlmax  33842  lcvexchlem4  34324  lcvexchlem5  34325  2at0mat0  34811  pmapjoin  35138  cdlemg17h  35956  dihlspsnat  36622  lzunuz  37331  dvdsrabdioph  37374  acongeq12d  37546  jm2.25  37566  rmydioph  37581  expdioph  37590  fnwe2val  37619  aomclem8  37631  brfvrcld2  37984  uneqsn  38321  ntrneixb  38393  ntrneix3  38395  ntrneix13  38397  sbcorgOLD  38740  unima  39346  disjinfi  39380  salexct  40552  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  nnfoctbdjlem  40672  nnfoctbdj  40673  iundjiun  40677  el1fzopredsuc  41335  iccpartgel  41365  divgcdoddALTV  41593  perfectALTVlem2  41631  lindslinindsimp2lem5  42251  ldepspr  42262