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  2994  sbcor  3090  sbcorg  3091  unjust  3217  elun  3364  elif  3638  ifbi  3647  elprg  3714  eltpg  3739  rabsnifsb  3762  rabrsndc  3764  preq12bg  3882  exmid01  4316  exmidsssnc  4321  swopolem  4431  soeq1  4441  sowlin  4446  ordtri2orexmid  4650  regexmidlemm  4659  regexmidlem1  4660  reg2exmidlema  4661  ordsoexmid  4689  ordtri2or2exmid  4698  ontri2orexmidim  4699  nn0suc  4731  nndceq0  4745  0elnn  4746  soinxp  4825  fununi  5429  funcnvuni  5430  fun11iun  5640  unpreima  5807  isosolem  6003  xporderlem  6440  poxp  6441  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  inffiexmid  7179  fidcenumlemrk  7237  isomni  7440  enomnilem  7442  finomni  7444  exmidomni  7446  fodjuomnilemres  7452  onntri45  7564  papeq1  7573  papcotr  7577  tapeq1  7582  netap  7584  2omotaplemap  7587  indpi  7673  ltexprlemloc  7938  addextpr  7952  ltsosr  8095  aptisr  8110  mulextsr1lem  8111  mulextsr1  8112  axpre-ltwlin  8214  axpre-apti  8216  axpre-mulext  8219  axltwlin  8357  axapti  8360  axsuploc  8362  reapval  8867  reapti  8870  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  reapneg  8888  reapcotr  8889  remulext1  8890  apreim  8894  apsym  8897  apcotr  8898  apadd1  8899  addext  8901  apneg  8902  nn1m1nn  9272  nn1gt1  9288  elznn0  9609  elz2  9666  nn0n0n1ge2b  9675  nneoor  9698  uztric  9894  ltxr  10127  fzsplit2  10404  fzsplit3  10407  uzsplit  10448  nelfzo  10508  fzospliti  10534  fzouzsplit  10537  exbtwnzlemstep  10631  exbtwnzlemex  10633  qavgle  10642  frec2uzled  10815  sq11ap  11094  swrdnd  11376  sqrt11ap  11748  abs00ap  11772  maxclpr  11932  minmax  11940  minclpr  11947  xrmaxiflemcom  11959  xrminmax  11975  xrminltinf  11982  sumeq1  12065  sumeq2  12069  fz1f1o  12085  summodc  12094  fsum3  12098  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  prodmodc  12289  fprodseq  12294  fprodcl2lem  12316  zeo3  12579  odd2np1lem  12583  dvdsprime  12844  coprm  12866  ennnfonelemrnh  13251  igsumvalx  13652  gsumfzval  13654  gsumpropd  13655  gsumpropd2  13656  gsumress  13658  gsum0g  13659  islring  14437  opprlring  14442  isdomn  14516  opprdomnbg  14521  znidom  14931  reopnap  15537  dich0  15643  reapef  15769  logrpap0b  15867  wilthlem1  15974  perfectlem2  15994  lgslem1  15999  upgrm  16221  upgr1or2  16222  upgr1elem1  16241  edgupgren  16262  usgruspgrben  16307  subupgr  16394  konigsberglem1  16609  decidi  16693  bj-nn0suc0  16846  bj-inf2vnlem2  16867  bj-nn0sucALT  16874  isomninnlem  16940  trilpolemlt1  16951  trirec0  16954