Theorem orbi12d 716

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

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  pm4.39  882  3orbi123d  1338  ifpbi123d  1440  cadbi123d  1513  eueq3  3213  sbcor  3311  unjust  3408  elun  3574  elprg  3984  eltpg  4014  rabsnifsb  4040  rabrsn  4042  preq12bg  4154  disji2  4389  disjprg  4398  disjxun  4400  opthneg  4681  swopolem  4764  sotrieq  4782  isso2i  4787  somin1  5233  fununi  5649  unpreima  6006  ordsucun  6652  funcnvuni  6746  fun11iun  6753  frxp  6906  xporderlem  6907  poxp  6908  fnwelem  6911  fnse  6913  oacan  7249  omword  7271  oeword  7291  oeoa  7298  qsdisj  7440  wemapso2lem  8067  brwdom  8082  cantnflem1  8194  r0weon  8443  infxpen  8445  sornom  8707  fin1ai  8723  isfin5  8729  isfin6  8730  sdom2en01  8732  enfin2i  8751  enfin1ai  8814  isfin5-2  8821  fin1a2lem7  8836  fin1a2lem11  8840  fin1a2lem13  8842  axdc3lem2  8881  engch  9053  eltskg  9175  tsken  9179  ltsonq  9394  addcanpr  9471  ltsosr  9518  axpre-lttri  9589  lemul1  10457  mulge0b  10475  mulle0b  10476  mulsuble0b  10477  nn1m1nn  10629  avgle  10854  nn0sub  10920  elznn0  10952  elz2  10954  nneo  11019  uztric  11180  mul2lt0bi  11402  ltxr  11415  xrrebnd  11463  xmulval  11518  xmulneg1  11555  ixxun  11651  iccsplit  11765  fzsplit2  11824  uzsplit  11866  nelfzo  11925  fzospliti  11950  fzouzsplit  11953  sqeqor  12388  swrdnd  12788  sumeq1  13755  sumeq2w  13758  sumeq2ii  13759  fz1f1o  13776  summo  13783  fsum  13786  prodeq1f  13962  prodeq2w  13966  prodeq2ii  13967  prodmo  13990  fprod  13995  ruclem12  14293  odd2np1lem  14364  dvdsprime  14637  coprm  14657  vdwapun  14924  vdwlem6  14936  vdwlem10  14940  mreexexlemd  15550  mreexexd  15554  istos  16281  tosso  16282  tsrlin  16465  tsrss  16469  isdomn  18518  prmirredlem  19064  domnchr  19103  zntoslem  19127  znfld  19131  fctop  20019  cctop  20021  ppttop  20022  pptbas  20023  isufil  20918  ufilss  20920  fixufil  20937  fin1aufil  20947  xpsdsval  21396  nlmmul0or  21686  pmltpclem1  22399  iundisj2  22502  mbfmax  22605  dvne0  22963  fta1glem2  23117  plymul0or  23234  ofmulrt  23235  quotval  23245  plydivlem3  23248  plydivlem4  23249  plydivex  23250  plydivalg  23252  quotlem  23253  aalioulem2  23289  quad2  23765  dcubic2  23770  dcubic  23772  dquartlem1  23777  dquart  23779  quart  23787  leibpilem2  23867  wilthlem1  23993  muval2  24061  perfectlem2  24158  lgslem1  24224  pntpbnd1  24424  legtrid  24636  legso  24644  ishlg  24647  lnhl  24660  symquadlem  24734  islmib  24829  isinag  24879  inaghl  24881  brbtwn2  24935  axcontlem2  24995  axcontlem4  24997  axcontlem11  25004  nb3graprlem2  25180  hashecclwwlkn1  25562  frgra2v  25727  h1datom  27235  atss  27999  atom1d  28006  atord  28041  chirred  28048  elimifd  28160  disji2f  28187  disjif2  28191  disjxpin  28198  iundisj2f  28200  disjunsn  28204  fzsplit3  28370  iundisj2fi  28373  f1ocnt  28376  resstos  28421  tleile  28422  trleile  28427  smatrcl  28622  fsumcvg4  28756  erdsze2lem2  29927  funpsstri  30406  soseq  30492  seglelin  30883  lineunray  30914  topdifinffinlem  31750  topdifinffin  31751  topdifinfeq  31753  mblfinlem2  31978  itg2addnclem2  31994  iblabsnclem  32005  ftc1anclem5  32021  fdc1  32075  unichnidl  32264  ispridl  32267  maxidlmax  32276  lcvexchlem4  32603  lcvexchlem5  32604  2at0mat0  33090  pmapjoin  33417  cdlemg17h  34235  dihlspsnat  34901  lzunuz  35610  dvdsrabdioph  35653  acongeq12d  35829  jm2.25  35854  rmydioph  35869  expdioph  35878  fnwe2val  35907  aomclem8  35919  brfvrcld2  36284  sbcorgOLD  36891  unima  37429  disjinfi  37468  salexct  38193  salexct2  38198  salexct3  38201  salgencntex  38202  salgensscntex  38203  nnfoctbdjlem  38293  nnfoctbdj  38294  iundjiun  38298  el1fzopredsuc  38722  iccpartgel  38743  divgcdoddALTV  38811  perfectALTVlem2  38844  nb3grprlem2  39455  lindslinindsimp2lem5  40308  ldepspr  40319