Theorem orbi12d 798

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

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  827  dcbid  843  ifpbi123d  998  3orbi123d  1345  dfbi3dc  1439  eueq3dc  2977  sbcor  3073  sbcorg  3074  unjust  3200  elun  3345  elif  3614  ifbi  3623  elprg  3686  eltpg  3711  rabrsndc  3734  preq12bg  3851  exmid01  4282  exmidsssnc  4287  swopolem  4396  soeq1  4406  sowlin  4411  ordtri2orexmid  4615  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  ordsoexmid  4654  ordtri2or2exmid  4663  ontri2orexmidim  4664  nn0suc  4696  nndceq0  4710  0elnn  4711  soinxp  4789  fununi  5389  funcnvuni  5390  fun11iun  5593  unpreima  5760  isosolem  5948  xporderlem  6377  poxp  6378  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  inffiexmid  7068  fidcenumlemrk  7121  isomni  7303  enomnilem  7305  finomni  7307  exmidomni  7309  fodjuomnilemres  7315  onntri45  7426  tapeq1  7438  netap  7440  2omotaplemap  7443  indpi  7529  ltexprlemloc  7794  addextpr  7808  ltsosr  7951  aptisr  7966  mulextsr1lem  7967  mulextsr1  7968  axpre-ltwlin  8070  axpre-apti  8072  axpre-mulext  8075  axltwlin  8214  axapti  8217  axsuploc  8219  reapval  8723  reapti  8726  reapmul1lem  8741  reapmul1  8742  reapadd1  8743  reapneg  8744  reapcotr  8745  remulext1  8746  apreim  8750  apsym  8753  apcotr  8754  apadd1  8755  addext  8757  apneg  8758  nn1m1nn  9128  nn1gt1  9144  elznn0  9461  elz2  9518  nn0n0n1ge2b  9526  nneoor  9549  uztric  9744  ltxr  9971  fzsplit2  10246  uzsplit  10288  nelfzo  10348  fzospliti  10374  fzouzsplit  10377  exbtwnzlemstep  10467  exbtwnzlemex  10469  qavgle  10478  frec2uzled  10651  sq11ap  10929  swrdnd  11191  sqrt11ap  11549  abs00ap  11573  maxclpr  11733  minmax  11741  minclpr  11748  xrmaxiflemcom  11760  xrminmax  11776  xrminltinf  11783  sumeq1  11866  sumeq2  11870  fz1f1o  11886  summodc  11894  fsum3  11898  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  prodmodc  12089  fprodseq  12094  fprodcl2lem  12116  zeo3  12379  odd2np1lem  12383  dvdsprime  12644  coprm  12666  ennnfonelemrnh  12987  igsumvalx  13422  gsumfzval  13424  gsumpropd  13425  gsumpropd2  13426  gsumress  13428  gsum0g  13429  islring  14156  isdomn  14233  opprdomnbg  14238  znidom  14621  reopnap  15220  dich0  15326  reapef  15452  logrpap0b  15550  wilthlem1  15654  perfectlem2  15674  lgslem1  15679  upgrm  15900  upgr1or2  15901  upgr1elem1  15920  edgupgren  15939  usgruspgrben  15984  decidi  16159  bj-nn0suc0  16313  bj-inf2vnlem2  16334  bj-nn0sucALT  16341  isomninnlem  16398  trilpolemlt1  16409  trirec0  16412