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  4337  exmidsssnc  4342  swopolem  4452  soeq1  4462  sowlin  4467  ordtri2orexmid  4672  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  ordsoexmid  4711  ordtri2or2exmid  4720  ontri2orexmidim  4721  nn0suc  4753  nndceq0  4767  0elnn  4768  soinxp  4847  fununi  5452  funcnvuni  5453  fun11iun  5663  unpreima  5836  isosolem  6033  xporderlem  6471  poxp  6472  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  inffiexmid  7217  fidcenumlemrk  7276  isomni  7482  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  onntri45  7606  papeq1  7615  papcotr  7619  tapeq1  7624  netap  7626  2omotaplemap  7629  indpi  7715  ltexprlemloc  7980  addextpr  7994  ltsosr  8137  aptisr  8152  mulextsr1lem  8153  mulextsr1  8154  axpre-ltwlin  8256  axpre-apti  8258  axpre-mulext  8261  axltwlin  8399  axapti  8402  axsuploc  8404  reapval  8912  reapti  8915  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  reapneg  8933  reapcotr  8934  remulext1  8935  apreim  8939  apsym  8942  apcotr  8943  apadd1  8944  addext  8946  apneg  8947  nn1m1nn  9331  nn1gt1  9347  elznn0  9670  elz2  9727  nn0n0n1ge2b  9736  nneoor  9759  uztric  9960  ltxr  10194  fzsplit2  10472  fzsplit3  10475  uzsplit  10516  nelfzo  10576  fzospliti  10602  fzouzsplit  10605  exbtwnzlemstep  10699  exbtwnzlemex  10701  qavgle  10710  frec2uzled  10887  sq11ap  11166  swrdnd  11453  sqrt11ap  11826  abs00ap  11850  maxclpr  12011  minmax  12020  minclpr  12027  xrmaxiflemcom  12040  xrminmax  12056  xrminltinf  12063  sumeq1  12146  sumeq2  12150  fz1f1o  12166  summodc  12175  fsum3  12179  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  prodmodc  12370  fprodseq  12375  fprodcl2lem  12397  zeo3  12660  odd2np1lem  12664  dvdsprime  12925  coprm  12948  ennnfonelemrnh  13365  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsum0  13772  islring  14608  opprlring  14613  isdomn  14687  opprdomnbg  14692  znidom  15101  reopnap  15772  dich0  15878  reapef  16004  logrpap0b  16106  zprmlogbap  16218  wilthlem1  16232  perfectlem2  16300  prmefexple  16308  bposlem1  16311  lgslem1  16324  upgrm  16546  upgr1or2  16547  upgr1elem1  16566  edgupgren  16587  usgruspgrben  16632  subupgr  16719  konigsberglem1  16934  dichmul0orlem3  16960  dichmul0orlem7  16964  decidi  17028  bj-nn0suc0  17181  bj-inf2vnlem2  17202  bj-nn0sucALT  17209  wexmiddc  17247  isomninnlem  17285  trilpolemlt1  17297  trirec0  17300