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  7378  enomnilem  7380  finomni  7382  exmidomni  7384  fodjuomnilemres  7390  onntri45  7502  tapeq1  7514  netap  7516  2omotaplemap  7519  indpi  7605  ltexprlemloc  7870  addextpr  7884  ltsosr  8027  aptisr  8042  mulextsr1lem  8043  mulextsr1  8044  axpre-ltwlin  8146  axpre-apti  8148  axpre-mulext  8151  axltwlin  8290  axapti  8293  axsuploc  8295  reapval  8799  reapti  8802  reapmul1lem  8817  reapmul1  8818  reapadd1  8819  reapneg  8820  reapcotr  8821  remulext1  8822  apreim  8826  apsym  8829  apcotr  8830  apadd1  8831  addext  8833  apneg  8834  nn1m1nn  9204  nn1gt1  9220  elznn0  9537  elz2  9594  nn0n0n1ge2b  9602  nneoor  9625  uztric  9821  ltxr  10053  fzsplit2  10328  uzsplit  10370  nelfzo  10430  fzospliti  10456  fzouzsplit  10459  exbtwnzlemstep  10551  exbtwnzlemex  10553  qavgle  10562  frec2uzled  10735  sq11ap  11013  swrdnd  11287  sqrt11ap  11659  abs00ap  11683  maxclpr  11843  minmax  11851  minclpr  11858  xrmaxiflemcom  11870  xrminmax  11886  xrminltinf  11893  sumeq1  11976  sumeq2  11980  fz1f1o  11996  summodc  12005  fsum3  12009  prodeq1f  12174  prodeq2w  12178  prodeq2  12179  prodmodc  12200  fprodseq  12205  fprodcl2lem  12227  zeo3  12490  odd2np1lem  12494  dvdsprime  12755  coprm  12777  ennnfonelemrnh  13098  igsumvalx  13533  gsumfzval  13535  gsumpropd  13536  gsumpropd2  13537  gsumress  13539  gsum0g  13540  islring  14268  isdomn  14345  opprdomnbg  14350  znidom  14733  reopnap  15337  dich0  15443  reapef  15569  logrpap0b  15667  wilthlem1  15771  perfectlem2  15791  lgslem1  15796  upgrm  16018  upgr1or2  16019  upgr1elem1  16038  edgupgren  16059  usgruspgrben  16104  subupgr  16191  konigsberglem1  16406  decidi  16490  bj-nn0suc0  16643  bj-inf2vnlem2  16664  bj-nn0sucALT  16671  isomninnlem  16739  trilpolemlt1  16750  trirec0  16753