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  2938  sbcor  3034  sbcorg  3035  unjust  3160  elun  3305  ifbi  3582  elprg  3643  eltpg  3668  rabrsndc  3691  preq12bg  3804  exmid01  4232  exmidsssnc  4237  swopolem  4341  soeq1  4351  sowlin  4356  ordtri2orexmid  4560  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  ordsoexmid  4599  ordtri2or2exmid  4608  ontri2orexmidim  4609  nn0suc  4641  nndceq0  4655  0elnn  4656  soinxp  4734  fununi  5327  funcnvuni  5328  fun11iun  5528  unpreima  5690  isosolem  5874  xporderlem  6298  poxp  6299  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  inffiexmid  6976  fidcenumlemrk  7029  isomni  7211  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  onntri45  7324  tapeq1  7335  netap  7337  2omotaplemap  7340  indpi  7426  ltexprlemloc  7691  addextpr  7705  ltsosr  7848  aptisr  7863  mulextsr1lem  7864  mulextsr1  7865  axpre-ltwlin  7967  axpre-apti  7969  axpre-mulext  7972  axltwlin  8111  axapti  8114  axsuploc  8116  reapval  8620  reapti  8623  reapmul1lem  8638  reapmul1  8639  reapadd1  8640  reapneg  8641  reapcotr  8642  remulext1  8643  apreim  8647  apsym  8650  apcotr  8651  apadd1  8652  addext  8654  apneg  8655  nn1m1nn  9025  nn1gt1  9041  elznn0  9358  elz2  9414  nn0n0n1ge2b  9422  nneoor  9445  uztric  9640  ltxr  9867  fzsplit2  10142  uzsplit  10184  nelfzo  10244  fzospliti  10269  fzouzsplit  10272  exbtwnzlemstep  10354  exbtwnzlemex  10356  qavgle  10365  frec2uzled  10538  sq11ap  10816  sqrt11ap  11220  abs00ap  11244  maxclpr  11404  minmax  11412  minclpr  11419  xrmaxiflemcom  11431  xrminmax  11447  xrminltinf  11454  sumeq1  11537  sumeq2  11541  fz1f1o  11557  summodc  11565  fsum3  11569  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  prodmodc  11760  fprodseq  11765  fprodcl2lem  11787  zeo3  12050  odd2np1lem  12054  dvdsprime  12315  coprm  12337  ennnfonelemrnh  12658  igsumvalx  13091  gsumfzval  13093  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  gsum0g  13098  islring  13824  isdomn  13901  opprdomnbg  13906  znidom  14289  reopnap  14866  dich0  14972  reapef  15098  logrpap0b  15196  wilthlem1  15300  perfectlem2  15320  lgslem1  15325  decidi  15525  bj-nn0suc0  15680  bj-inf2vnlem2  15701  bj-nn0sucALT  15708  isomninnlem  15761  trilpolemlt1  15772  trirec0  15775