Theorem orbi12d 707

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

Syntax hints:   -> wi 4   <-> wb 98   \/ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.39  735  dcbid  748  3orbi123d  1206  dfbi3dc  1288  eueq3dc  2715  sbcor  2807  sbcorg  2808  unjust  2921  elun  3084  ifbi  3348  elprg  3395  eltpg  3416  rabrsndc  3438  preq12bg  3544  swopolem  4042  soeq1  4052  sowlin  4057  ordtri2orexmid  4248  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  ordsoexmid  4286  ordtri2or2exmid  4296  nn0suc  4327  nndceq0  4339  0elnn  4340  soinxp  4410  fununi  4967  funcnvuni  4968  fun11iun  5147  unpreima  5292  isosolem  5463  xporderlem  5852  poxp  5853  frec0g  5983  frecsuclem3  5990  frecsuc  5991  indpi  6440  ltexprlemloc  6705  addextpr  6719  ltsosr  6849  aptisr  6863  mulextsr1lem  6864  mulextsr1  6865  axpre-ltwlin  6957  axpre-apti  6959  axpre-mulext  6962  axltwlin  7087  axapti  7090  reapval  7567  reapti  7570  reapmul1lem  7585  reapmul1  7586  reapadd1  7587  reapneg  7588  reapcotr  7589  remulext1  7590  apreim  7594  apsym  7597  apcotr  7598  apadd1  7599  addext  7601  apneg  7602  nn1m1nn  7932  nn1gt1  7947  elznn0  8260  elz2  8312  nn0n0n1ge2b  8320  nneoor  8340  uztric  8494  ltxr  8695  fzsplit2  8914  uzsplit  8954  fzospliti  9032  fzouzsplit  9035  sq11ap  9414  sqrt11ap  9636  abs00ap  9660  sumeq1  9874  bj-dcbi  10048  bj-nn0suc0  10075  bj-inf2vnlem2  10096  bj-nn0sucALT  10103