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  8906  reapti  8909  reapmul1lem  8924  reapmul1  8925  reapadd1  8926  reapneg  8927  reapcotr  8928  remulext1  8929  apreim  8933  apsym  8936  apcotr  8937  apadd1  8938  addext  8940  apneg  8941  nn1m1nn  9324  nn1gt1  9340  elznn0  9663  elz2  9720  nn0n0n1ge2b  9729  nneoor  9752  uztric  9953  ltxr  10187  fzsplit2  10465  fzsplit3  10468  uzsplit  10509  nelfzo  10569  fzospliti  10595  fzouzsplit  10598  exbtwnzlemstep  10692  exbtwnzlemex  10694  qavgle  10703  frec2uzled  10879  sq11ap  11158  swrdnd  11445  sqrt11ap  11818  abs00ap  11842  maxclpr  12003  minmax  12011  minclpr  12018  xrmaxiflemcom  12031  xrminmax  12047  xrminltinf  12054  sumeq1  12137  sumeq2  12141  fz1f1o  12157  summodc  12166  fsum3  12170  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  prodmodc  12361  fprodseq  12366  fprodcl2lem  12388  zeo3  12651  odd2np1lem  12655  dvdsprime  12916  coprm  12939  ennnfonelemrnh  13356  gzsumvalx  13758  gzsumfzval  13760  gzsumress  13761  gzsum0  13762  islring  14548  opprlring  14553  isdomn  14627  opprdomnbg  14632  znidom  15041  reopnap  15696  dich0  15802  reapef  15928  logrpap0b  16028  zprmlogbap  16137  wilthlem1  16151  perfectlem2  16198  prmefexple  16206  bposlem1  16209  lgslem1  16217  upgrm  16439  upgr1or2  16440  upgr1elem1  16459  edgupgren  16480  usgruspgrben  16525  subupgr  16612  konigsberglem1  16827  dichmul0orlem3  16853  dichmul0orlem7  16857  decidi  16921  bj-nn0suc0  17074  bj-inf2vnlem2  17095  bj-nn0sucALT  17102  wexmiddc  17140  isomninnlem  17177  trilpolemlt1  17188  trirec0  17191