Theorem orbi12d 748

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

Syntax hints:   -> wi 4   <-> wb 104   \/ wo 670

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  777  dcbid  792  3orbi123d  1257  dfbi3dc  1343  eueq3dc  2811  sbcor  2905  sbcorg  2906  unjust  3024  elun  3164  ifbi  3439  elprg  3494  eltpg  3516  rabrsndc  3538  preq12bg  3647  exmid01  4061  exmidsssnc  4064  swopolem  4165  soeq1  4175  sowlin  4180  ordtri2orexmid  4376  regexmidlemm  4385  regexmidlem1  4386  reg2exmidlema  4387  ordsoexmid  4415  ordtri2or2exmid  4424  nn0suc  4456  nndceq0  4469  0elnn  4470  soinxp  4547  fununi  5127  funcnvuni  5128  fun11iun  5322  unpreima  5477  isosolem  5657  xporderlem  6058  poxp  6059  frec0g  6224  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  inffiexmid  6729  fidcenumlemrk  6770  isomni  6920  enomnilem  6922  finomni  6924  exmidomni  6926  fodjuomnilemres  6932  indpi  7051  ltexprlemloc  7316  addextpr  7330  ltsosr  7460  aptisr  7474  mulextsr1lem  7475  mulextsr1  7476  axpre-ltwlin  7568  axpre-apti  7570  axpre-mulext  7573  axltwlin  7704  axapti  7707  reapval  8204  reapti  8207  reapmul1lem  8222  reapmul1  8223  reapadd1  8224  reapneg  8225  reapcotr  8226  remulext1  8227  apreim  8231  apsym  8234  apcotr  8235  apadd1  8236  addext  8238  apneg  8239  nn1m1nn  8596  nn1gt1  8612  elznn0  8921  elz2  8974  nn0n0n1ge2b  8982  nneoor  9005  uztric  9197  ltxr  9403  fzsplit2  9671  uzsplit  9713  fzospliti  9794  fzouzsplit  9797  exbtwnzlemstep  9866  exbtwnzlemex  9868  qavgle  9877  frec2uzled  10043  sq11ap  10299  sqrt11ap  10650  abs00ap  10674  maxclpr  10834  minmax  10840  minclpr  10847  xrmaxiflemcom  10857  xrminmax  10873  xrminltinf  10880  sumeq1  10963  sumeq2  10967  fz1f1o  10983  summodc  10991  fsum3  10995  zeo3  11360  odd2np1lem  11364  dvdsprime  11596  coprm  11615  ennnfonelemrnh  11721  decidi  12583  bj-dcbi  12707  bj-nn0suc0  12733  bj-inf2vnlem2  12754  bj-nn0sucALT  12761  isomninnlem  12809  trilpolemlt1  12818