Theorem orbi12d 783

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  812  dcbid  828  3orbi123d  1301  dfbi3dc  1387  eueq3dc  2900  sbcor  2995  sbcorg  2996  unjust  3119  elun  3263  ifbi  3540  elprg  3596  eltpg  3621  rabrsndc  3644  preq12bg  3753  exmid01  4177  exmidsssnc  4182  swopolem  4283  soeq1  4293  sowlin  4298  ordtri2orexmid  4500  regexmidlemm  4509  regexmidlem1  4510  reg2exmidlema  4511  ordsoexmid  4539  ordtri2or2exmid  4548  ontri2orexmidim  4549  nn0suc  4581  nndceq0  4595  0elnn  4596  soinxp  4674  fununi  5256  funcnvuni  5257  fun11iun  5453  unpreima  5610  isosolem  5792  xporderlem  6199  poxp  6200  frec0g  6365  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  inffiexmid  6872  fidcenumlemrk  6919  isomni  7100  enomnilem  7102  finomni  7104  exmidomni  7106  fodjuomnilemres  7112  onntri45  7197  indpi  7283  ltexprlemloc  7548  addextpr  7562  ltsosr  7705  aptisr  7720  mulextsr1lem  7721  mulextsr1  7722  axpre-ltwlin  7824  axpre-apti  7826  axpre-mulext  7829  axltwlin  7966  axapti  7969  axsuploc  7971  reapval  8474  reapti  8477  reapmul1lem  8492  reapmul1  8493  reapadd1  8494  reapneg  8495  reapcotr  8496  remulext1  8497  apreim  8501  apsym  8504  apcotr  8505  apadd1  8506  addext  8508  apneg  8509  nn1m1nn  8875  nn1gt1  8891  elznn0  9206  elz2  9262  nn0n0n1ge2b  9270  nneoor  9293  uztric  9487  ltxr  9711  fzsplit2  9985  uzsplit  10027  fzospliti  10111  fzouzsplit  10114  exbtwnzlemstep  10183  exbtwnzlemex  10185  qavgle  10194  frec2uzled  10364  sq11ap  10622  sqrt11ap  10980  abs00ap  11004  maxclpr  11164  minmax  11171  minclpr  11178  xrmaxiflemcom  11190  xrminmax  11206  xrminltinf  11213  sumeq1  11296  sumeq2  11300  fz1f1o  11316  summodc  11324  fsum3  11328  prodeq1f  11493  prodeq2w  11497  prodeq2  11498  prodmodc  11519  fprodseq  11524  fprodcl2lem  11546  zeo3  11805  odd2np1lem  11809  dvdsprime  12054  coprm  12076  ennnfonelemrnh  12349  reopnap  13178  reapef  13339  logrpap0b  13437  lgslem1  13541  decidi  13676  bj-nn0suc0  13832  bj-inf2vnlem2  13853  bj-nn0sucALT  13860  isomninnlem  13909  trilpolemlt1  13920  trirec0  13923