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  1289  cadbi123d  1425  eueq3  3241  sbcor  3339  sbcorgOLD  3340  unjust  3443  elun  3608  elprg  4004  eltpg  4029  rabsnifsb  4054  rabrsn  4056  preq12bg  4162  disji2  4390  disjprg  4399  disjxun  4401  opthneg  4682  swopolem  4761  sotrieq  4779  isso2i  4784  somin1  5345  fununi  5595  unpreima  5941  ordsucun  6549  funcnvuni  6643  fun11iun  6650  frxp  6795  xporderlem  6796  poxp  6797  fnwelem  6800  fnse  6802  oacan  7100  omword  7122  oeword  7142  oeoa  7149  qsdisj  7290  wemapso2OLD  7880  wemapso2lem  7881  brwdom  7896  cantnflem1  8011  cantnflem1OLD  8034  r0weon  8293  infxpen  8295  sornom  8560  fin1ai  8576  isfin5  8582  isfin6  8583  sdom2en01  8585  enfin2i  8604  enfin1ai  8667  isfin5-2  8674  fin1a2lem7  8689  fin1a2lem11  8693  fin1a2lem13  8695  axdc3lem2  8734  engch  8909  eltskg  9031  tsken  9035  ltsonq  9252  addcanpr  9329  ltsosr  9375  axpre-lttri  9446  lemul1  10295  mulge0b  10313  mulle0b  10314  mulsuble0b  10315  nn1m1nn  10456  avgle  10680  nn0sub  10744  elznn0  10775  elz2  10777  nneo  10839  uztric  10996  ltxr  11209  xrrebnd  11254  xmulval  11309  xmulneg1  11346  ixxun  11430  iccsplit  11538  fzsplit2  11594  uzsplit  11650  fzospliti  11701  fzouzsplit  11704  sqeqor  12100  sumeq1  13287  sumeq2w  13290  sumeq2ii  13291  fz1f1o  13308  summo  13315  fsum  13318  ruclem12  13644  odd2np1lem  13712  dvdsprime  13897  coprm  13907  vdwapun  14156  vdwlem6  14168  vdwlem10  14172  mreexexlemd  14704  mreexexd  14708  istos  15327  tosso  15328  tsrlin  15511  tsrss  15515  isdomn  17492  prmirredlem  18045  prmirredlemOLD  18048  domnchr  18091  zntoslem  18117  znfld  18121  fctop  18743  cctop  18745  ppttop  18746  pptbas  18747  isufil  19611  ufilss  19613  fixufil  19630  fin1aufil  19640  xpsdsval  20091  nlmmul0or  20399  pmltpclem1  21067  iundisj2  21166  mbfmax  21263  dvne0  21619  fta1glem2  21774  plymul0or  21883  ofmulrt  21884  quotval  21894  plydivlem3  21897  plydivlem4  21898  plydivex  21899  plydivalg  21901  quotlem  21902  aalioulem2  21935  quad2  22370  dcubic2  22375  dcubic  22377  dquartlem1  22382  dquart  22384  quart  22392  leibpilem2  22472  wilthlem1  22542  muval2  22608  perfectlem2  22705  lgslem1  22771  pntpbnd1  22971  legtrid  23163  symquadlem  23227  islmib  23279  brbtwn2  23323  axcontlem2  23383  axcontlem4  23385  axcontlem11  23392  nb3graprlem2  23532  h1datom  25157  atss  25922  atom1d  25929  atord  25964  chirred  25971  elimifd  26076  disji2f  26092  disjif2  26096  disjxpin  26101  iundisj2f  26103  disjunsn  26107  mul2lt0bi  26213  fzsplit3  26243  iundisj2fi  26246  resstos  26286  tleile  26287  trleile  26292  fsumcvg4  26545  erdsze2lem2  27256  prodeq1f  27585  prodeq2w  27589  prodeq2ii  27590  prodmo  27613  fprod  27618  funpsstri  27740  soseq  27879  seglelin  28311  lineunray  28342  mblfinlem2  28597  itg2addnclem2  28612  iblabsnclem  28623  ftc1anclem5  28639  fdc1  28810  unichnidl  28999  ispridl  29002  maxidlmax  29011  lzunuz  29274  dvdsrabdioph  29316  acongeq12d  29490  jm2.25  29516  rmydioph  29531  expdioph  29540  fnwe2val  29570  aomclem8  29582  hashecclwwlkn1  30676  frgra2v  30759  lindslinindsimp2lem5  31148  ldepspr  31159  lcvexchlem4  33040  lcvexchlem5  33041  2at0mat0  33527  pmapjoin  33854  cdlemg17h  34670  dihlspsnat  35336