Theorem orbi12d 794

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  823  dcbid  839  3orbi123d  1322  dfbi3dc  1408  eueq3dc  2926  sbcor  3022  sbcorg  3023  unjust  3147  elun  3291  ifbi  3569  elprg  3630  eltpg  3655  rabrsndc  3678  preq12bg  3791  exmid01  4219  exmidsssnc  4224  swopolem  4326  soeq1  4336  sowlin  4341  ordtri2orexmid  4543  regexmidlemm  4552  regexmidlem1  4553  reg2exmidlema  4554  ordsoexmid  4582  ordtri2or2exmid  4591  ontri2orexmidim  4592  nn0suc  4624  nndceq0  4638  0elnn  4639  soinxp  4717  fununi  5306  funcnvuni  5307  fun11iun  5504  unpreima  5665  isosolem  5849  xporderlem  6260  poxp  6261  frec0g  6426  freccllem  6431  frecfcllem  6433  frecsuclem  6435  frecsuc  6436  inffiexmid  6938  fidcenumlemrk  6987  isomni  7169  enomnilem  7171  finomni  7173  exmidomni  7175  fodjuomnilemres  7181  onntri45  7275  tapeq1  7286  netap  7288  2omotaplemap  7291  indpi  7376  ltexprlemloc  7641  addextpr  7655  ltsosr  7798  aptisr  7813  mulextsr1lem  7814  mulextsr1  7815  axpre-ltwlin  7917  axpre-apti  7919  axpre-mulext  7922  axltwlin  8060  axapti  8063  axsuploc  8065  reapval  8568  reapti  8571  reapmul1lem  8586  reapmul1  8587  reapadd1  8588  reapneg  8589  reapcotr  8590  remulext1  8591  apreim  8595  apsym  8598  apcotr  8599  apadd1  8600  addext  8602  apneg  8603  nn1m1nn  8972  nn1gt1  8988  elznn0  9303  elz2  9359  nn0n0n1ge2b  9367  nneoor  9390  uztric  9585  ltxr  9811  fzsplit2  10086  uzsplit  10128  fzospliti  10212  fzouzsplit  10215  exbtwnzlemstep  10284  exbtwnzlemex  10286  qavgle  10295  frec2uzled  10466  sq11ap  10728  sqrt11ap  11088  abs00ap  11112  maxclpr  11272  minmax  11279  minclpr  11286  xrmaxiflemcom  11298  xrminmax  11314  xrminltinf  11321  sumeq1  11404  sumeq2  11408  fz1f1o  11424  summodc  11432  fsum3  11436  prodeq1f  11601  prodeq2w  11605  prodeq2  11606  prodmodc  11627  fprodseq  11632  fprodcl2lem  11654  zeo3  11914  odd2np1lem  11918  dvdsprime  12165  coprm  12187  ennnfonelemrnh  12478  igsumvalx  12876  gsumpropd  12878  gsumpropd2  12879  gsumress  12881  gsum0g  12882  islring  13564  reopnap  14523  reapef  14684  logrpap0b  14782  wilthlem1  14883  lgslem1  14887  decidi  15033  bj-nn0suc0  15188  bj-inf2vnlem2  15209  bj-nn0sucALT  15216  isomninnlem  15266  trilpolemlt1  15277  trirec0  15280