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  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  inffiexmid  7219  fidcenumlemrk  7278  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  9668  elz2  9725  nn0n0n1ge2b  9734  nneoor  9758  uztric  9959  ltxr  10193  fzsplit2  10471  fzsplit3  10474  uzsplit  10515  nelfzo  10575  fzospliti  10601  fzouzsplit  10604  exbtwnzlemstep  10698  exbtwnzlemex  10700  qavgle  10709  frec2uzled  10886  sq11ap  11165  swrdnd  11452  sqrt11ap  11825  abs00ap  11849  maxclpr  12010  minmax  12019  minclpr  12026  xrmaxiflemcom  12039  xrminmax  12055  xrminltinf  12062  sumeq1  12145  sumeq2  12149  fz1f1o  12165  summodc  12174  fsum3  12178  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  prodmodc  12369  fprodseq  12374  fprodcl2lem  12396  zeo3  12659  odd2np1lem  12663  dvdsprime  12924  coprm  12947  ennnfonelemrnh  13364  gzsumvalx  13767  gzsumfzval  13769  gzsumress  13770  gzsum0  13771  islring  14607  opprlring  14612  isdomn  14686  opprdomnbg  14691  znidom  15100  reopnap  15789  dich0  15895  reapef  16021  logrpap0b  16123  zprmlogbap  16235  wilthlem1  16249  perfectlem2  16317  prmefexple  16325  bposlem1  16328  lgslem1  16341  upgrm  16563  upgr1or2  16564  upgr1elem1  16583  edgupgren  16604  usgruspgrben  16649  subupgr  16736  konigsberglem1  16951  dichmul0orlem3  16977  dichmul0orlem7  16981  decidi  17045  bj-nn0suc0  17198  bj-inf2vnlem2  17219  bj-nn0sucALT  17226  wexmiddc  17264  isomninnlem  17302  trilpolemlt1  17314  trirec0  17317