Theorem orbi12d 805

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12d.1	|- ( ph -> ( ps <-> ch ) )
orbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
orbi12d	|- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		orbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	orbi1d 803	. 2 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
3		orbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	orbi2d 802	. 2 |- ( ph -> ( ( ch \/ th ) <-> ( ch \/ ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.39  834  dcbid  850  ifpbi123d  1005  3orbi123d  1352  dfbi3dc  1446  eueq3dc  3000  sbcor  3096  sbcorg  3097  unjust  3223  elun  3370  elif  3652  ifbi  3661  elprg  3729  eltpg  3754  rabsnifsb  3777  rabrsndc  3779  preq12bg  3898  exmid01  4335  exmidsssnc  4340  swopolem  4450  soeq1  4460  sowlin  4465  ordtri2orexmid  4670  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  ordsoexmid  4709  ordtri2or2exmid  4718  ontri2orexmidim  4719  nn0suc  4751  nndceq0  4765  0elnn  4766  soinxp  4845  fununi  5449  funcnvuni  5450  fun11iun  5660  unpreima  5833  isosolem  6030  xporderlem  6467  poxp  6468  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  inffiexmid  7213  fidcenumlemrk  7271  isomni  7476  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  onntri45  7600  papeq1  7609  papcotr  7613  tapeq1  7618  netap  7620  2omotaplemap  7623  indpi  7709  ltexprlemloc  7974  addextpr  7988  ltsosr  8131  aptisr  8146  mulextsr1lem  8147  mulextsr1  8148  axpre-ltwlin  8250  axpre-apti  8252  axpre-mulext  8255  axltwlin  8393  axapti  8396  axsuploc  8398  reapval  8904  reapti  8907  reapmul1lem  8922  reapmul1  8923  reapadd1  8924  reapneg  8925  reapcotr  8926  remulext1  8927  apreim  8931  apsym  8934  apcotr  8935  apadd1  8936  addext  8938  apneg  8939  nn1m1nn  9322  nn1gt1  9338  elznn0  9659  elz2  9716  nn0n0n1ge2b  9725  nneoor  9748  uztric  9944  ltxr  10177  fzsplit2  10455  fzsplit3  10458  uzsplit  10499  nelfzo  10559  fzospliti  10585  fzouzsplit  10588  exbtwnzlemstep  10682  exbtwnzlemex  10684  qavgle  10693  frec2uzled  10866  sq11ap  11145  swrdnd  11431  sqrt11ap  11804  abs00ap  11828  maxclpr  11988  minmax  11996  minclpr  12003  xrmaxiflemcom  12015  xrminmax  12031  xrminltinf  12038  sumeq1  12121  sumeq2  12125  fz1f1o  12141  summodc  12150  fsum3  12154  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  prodmodc  12345  fprodseq  12350  fprodcl2lem  12372  zeo3  12635  odd2np1lem  12639  dvdsprime  12900  coprm  12922  ennnfonelemrnh  13307  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsum0  13713  islring  14499  opprlring  14504  isdomn  14578  opprdomnbg  14583  znidom  14992  reopnap  15647  dich0  15753  reapef  15879  logrpap0b  15977  wilthlem1  16094  perfectlem2  16114  lgslem1  16119  upgrm  16341  upgr1or2  16342  upgr1elem1  16361  edgupgren  16382  usgruspgrben  16427  subupgr  16514  konigsberglem1  16729  dichmul0orlem3  16755  dichmul0orlem7  16759  decidi  16823  bj-nn0suc0  16976  bj-inf2vnlem2  16997  bj-nn0sucALT  17004  wexmiddc  17042  isomninnlem  17079  trilpolemlt1  17090  trirec0  17093