Theorem orbi12d 724

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

Syntax hints:   -> wi 4   <-> wb 189   \/ wo 375

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 190  df-or 377

This theorem is referenced by:  pm4.39  888  ifpbi123d  998  3orbi123d  1364  cadbi123d  1521  eueq3  3201  sbcor  3299  unjust  3394  elun  3565  elprg  3975  eltpg  4005  rabsnifsb  4031  rabrsn  4033  preq12bg  4146  disji2  4382  disjprg  4391  disjxun  4393  opthneg  4681  swopolem  4769  sotrieq  4787  isso2i  4792  somin1  5239  fununi  5659  unpreima  6021  ordsucun  6671  funcnvuni  6765  fun11iun  6772  frxp  6925  xporderlem  6926  poxp  6927  fnwelem  6930  fnse  6932  oacan  7267  omword  7289  oeword  7309  oeoa  7316  qsdisj  7458  wemapso2lem  8085  brwdom  8100  cantnflem1  8212  r0weon  8461  infxpen  8463  sornom  8725  fin1ai  8741  isfin5  8747  isfin6  8748  sdom2en01  8750  enfin2i  8769  enfin1ai  8832  isfin5-2  8839  fin1a2lem7  8854  fin1a2lem11  8858  fin1a2lem13  8860  axdc3lem2  8899  engch  9071  eltskg  9193  tsken  9197  ltsonq  9412  addcanpr  9489  ltsosr  9536  axpre-lttri  9607  lemul1  10479  mulge0b  10497  mulle0b  10498  mulsuble0b  10499  nn1m1nn  10651  avgle  10877  nn0sub  10944  elznn0  10976  elz2  10978  nneo  11042  uztric  11204  mul2lt0bi  11425  ltxr  11438  xrrebnd  11486  xmulval  11541  xmulneg1  11580  ixxun  11676  iccsplit  11791  fzsplit2  11850  uzsplit  11892  nelfzo  11952  fzospliti  11977  fzouzsplit  11980  sqeqor  12426  swrdnd  12842  sumeq1  13832  sumeq2w  13835  sumeq2ii  13836  fz1f1o  13853  summo  13860  fsum  13863  prodeq1f  14039  prodeq2w  14043  prodeq2ii  14044  prodmo  14067  fprod  14072  ruclem12  14370  odd2np1lem  14442  dvdsprime  14716  coprm  14736  vdwapun  15003  vdwlem6  15015  vdwlem10  15019  mreexexlemd  15628  mreexexd  15632  istos  16359  tosso  16360  tsrlin  16543  tsrss  16547  isdomn  18595  prmirredlem  19141  domnchr  19180  zntoslem  19204  znfld  19208  fctop  20096  cctop  20098  ppttop  20099  pptbas  20100  isufil  20996  ufilss  20998  fixufil  21015  fin1aufil  21025  xpsdsval  21474  nlmmul0or  21764  pmltpclem1  22477  iundisj2  22581  mbfmax  22684  dvne0  23042  fta1glem2  23196  plymul0or  23313  ofmulrt  23314  quotval  23324  plydivlem3  23327  plydivlem4  23328  plydivex  23329  plydivalg  23331  quotlem  23332  aalioulem2  23368  quad2  23844  dcubic2  23849  dcubic  23851  dquartlem1  23856  dquart  23858  quart  23866  leibpilem2  23946  wilthlem1  24072  muval2  24140  perfectlem2  24237  lgslem1  24303  pntpbnd1  24503  legtrid  24715  legso  24723  ishlg  24726  lnhl  24739  symquadlem  24813  islmib  24908  isinag  24958  inaghl  24960  brbtwn2  25014  axcontlem2  25074  axcontlem4  25076  axcontlem11  25083  nb3graprlem2  25259  hashecclwwlkn1  25641  frgra2v  25806  h1datom  27316  atss  28080  atom1d  28087  atord  28122  chirred  28129  elimifd  28238  disji2f  28264  disjif2  28268  disjxpin  28275  iundisj2f  28277  disjunsn  28281  fzsplit3  28445  iundisj2fi  28448  f1ocnt  28451  resstos  28496  tleile  28497  trleile  28502  smatrcl  28696  fsumcvg4  28830  erdsze2lem2  29999  funpsstri  30477  soseq  30563  seglelin  30954  lineunray  30985  topdifinffinlem  31820  topdifinffin  31821  topdifinfeq  31823  mblfinlem2  32042  itg2addnclem2  32058  iblabsnclem  32069  ftc1anclem5  32085  fdc1  32139  unichnidl  32328  ispridl  32331  maxidlmax  32340  lcvexchlem4  32674  lcvexchlem5  32675  2at0mat0  33161  pmapjoin  33488  cdlemg17h  34306  dihlspsnat  34972  lzunuz  35681  dvdsrabdioph  35724  acongeq12d  35900  jm2.25  35925  rmydioph  35940  expdioph  35949  fnwe2val  35978  aomclem8  35990  brfvrcld2  36355  sbcorgOLD  36961  unima  37502  disjinfi  37539  salexct  38305  salexct2  38310  salexct3  38313  salgencntex  38314  salgensscntex  38315  nnfoctbdjlem  38409  nnfoctbdj  38410  iundjiun  38414  el1fzopredsuc  38867  iccpartgel  38888  divgcdoddALTV  38956  perfectALTVlem2  38989  nb3grprlem2  39619  lindslinindsimp2lem5  40763  ldepspr  40774