Theorem orbi12d 739

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

Syntax hints:   -> wi 4   <-> wb 103   \/ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.39  768  dcbid  781  3orbi123d  1242  dfbi3dc  1328  eueq3dc  2766  sbcor  2858  sbcorg  2859  unjust  2976  elun  3113  ifbi  3369  elprg  3418  eltpg  3438  rabrsndc  3460  preq12bg  3565  swopolem  4060  soeq1  4070  sowlin  4075  ordtri2orexmid  4266  regexmidlemm  4275  regexmidlem1  4276  reg2exmidlema  4277  ordsoexmid  4305  ordtri2or2exmid  4314  nn0suc  4345  nndceq0  4357  0elnn  4358  soinxp  4428  fununi  4987  funcnvuni  4988  fun11iun  5167  unpreima  5313  isosolem  5483  xporderlem  5872  poxp  5873  frec0g  6006  frecsuclem3  6013  frecsuc  6014  indpi  6532  ltexprlemloc  6797  addextpr  6811  ltsosr  6941  aptisr  6955  mulextsr1lem  6956  mulextsr1  6957  axpre-ltwlin  7049  axpre-apti  7051  axpre-mulext  7054  axltwlin  7180  axapti  7183  reapval  7676  reapti  7679  reapmul1lem  7694  reapmul1  7695  reapadd1  7696  reapneg  7697  reapcotr  7698  remulext1  7699  apreim  7703  apsym  7706  apcotr  7707  apadd1  7708  addext  7710  apneg  7711  nn1m1nn  8057  nn1gt1  8072  elznn0  8366  elz2  8419  nn0n0n1ge2b  8427  nneoor  8449  uztric  8640  ltxr  8849  fzsplit2  9069  uzsplit  9109  fzospliti  9185  fzouzsplit  9188  qavgle  9267  sq11ap  9639  sqrt11ap  9924  abs00ap  9948  maxclpr  10108  minmax  10112  sumeq1  10192  zeo3  10267  odd2np1lem  10271  dvdsprime  10504  coprm  10523  bj-dcbi  10719  bj-nn0suc0  10745  bj-inf2vnlem2  10766  bj-nn0sucALT  10773