Theorem orbi12d 801

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 799	. 2 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
3		orbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	orbi2d 798	. 2 |- ( ph -> ( ( ch \/ th ) <-> ( ch \/ ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  830  dcbid  846  ifpbi123d  1001  3orbi123d  1348  dfbi3dc  1442  eueq3dc  2981  sbcor  3077  sbcorg  3078  unjust  3204  elun  3350  elif  3621  ifbi  3630  elprg  3693  eltpg  3718  rabsnifsb  3741  rabrsndc  3743  preq12bg  3861  exmid01  4294  exmidsssnc  4299  swopolem  4408  soeq1  4418  sowlin  4423  ordtri2orexmid  4627  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  ordsoexmid  4666  ordtri2or2exmid  4675  ontri2orexmidim  4676  nn0suc  4708  nndceq0  4722  0elnn  4723  soinxp  4802  fununi  5405  funcnvuni  5406  fun11iun  5613  unpreima  5780  isosolem  5975  xporderlem  6405  poxp  6406  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  inffiexmid  7141  fidcenumlemrk  7196  isomni  7395  enomnilem  7397  finomni  7399  exmidomni  7401  fodjuomnilemres  7407  onntri45  7519  tapeq1  7531  netap  7533  2omotaplemap  7536  indpi  7622  ltexprlemloc  7887  addextpr  7901  ltsosr  8044  aptisr  8059  mulextsr1lem  8060  mulextsr1  8061  axpre-ltwlin  8163  axpre-apti  8165  axpre-mulext  8168  axltwlin  8306  axapti  8309  axsuploc  8311  reapval  8815  reapti  8818  reapmul1lem  8833  reapmul1  8834  reapadd1  8835  reapneg  8836  reapcotr  8837  remulext1  8838  apreim  8842  apsym  8845  apcotr  8846  apadd1  8847  addext  8849  apneg  8850  nn1m1nn  9220  nn1gt1  9236  elznn0  9555  elz2  9612  nn0n0n1ge2b  9620  nneoor  9643  uztric  9839  ltxr  10071  fzsplit2  10347  uzsplit  10389  nelfzo  10449  fzospliti  10475  fzouzsplit  10478  exbtwnzlemstep  10570  exbtwnzlemex  10572  qavgle  10581  frec2uzled  10754  sq11ap  11032  swrdnd  11306  sqrt11ap  11678  abs00ap  11702  maxclpr  11862  minmax  11870  minclpr  11877  xrmaxiflemcom  11889  xrminmax  11905  xrminltinf  11912  sumeq1  11995  sumeq2  11999  fz1f1o  12015  summodc  12024  fsum3  12028  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  prodmodc  12219  fprodseq  12224  fprodcl2lem  12246  zeo3  12509  odd2np1lem  12513  dvdsprime  12774  coprm  12796  ennnfonelemrnh  13117  igsumvalx  13552  gsumfzval  13554  gsumpropd  13555  gsumpropd2  13556  gsumress  13558  gsum0g  13559  islring  14287  isdomn  14365  opprdomnbg  14370  znidom  14753  reopnap  15357  dich0  15463  reapef  15589  logrpap0b  15687  wilthlem1  15794  perfectlem2  15814  lgslem1  15819  upgrm  16041  upgr1or2  16042  upgr1elem1  16061  edgupgren  16082  usgruspgrben  16127  subupgr  16214  konigsberglem1  16429  decidi  16513  bj-nn0suc0  16666  bj-inf2vnlem2  16687  bj-nn0sucALT  16694  isomninnlem  16762  trilpolemlt1  16773  trirec0  16776