Theorem orbi12d 782

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

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

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.39  811  dcbid  823  3orbi123d  1289  dfbi3dc  1375  eueq3dc  2858  sbcor  2953  sbcorg  2954  unjust  3074  elun  3217  ifbi  3492  elprg  3547  eltpg  3569  rabrsndc  3591  preq12bg  3700  exmid01  4121  exmidsssnc  4126  swopolem  4227  soeq1  4237  sowlin  4242  ordtri2orexmid  4438  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  ordsoexmid  4477  ordtri2or2exmid  4486  nn0suc  4518  nndceq0  4531  0elnn  4532  soinxp  4609  fununi  5191  funcnvuni  5192  fun11iun  5388  unpreima  5545  isosolem  5725  xporderlem  6128  poxp  6129  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  inffiexmid  6800  fidcenumlemrk  6842  isomni  7008  enomnilem  7010  finomni  7012  exmidomni  7014  fodjuomnilemres  7020  indpi  7150  ltexprlemloc  7415  addextpr  7429  ltsosr  7572  aptisr  7587  mulextsr1lem  7588  mulextsr1  7589  axpre-ltwlin  7691  axpre-apti  7693  axpre-mulext  7696  axltwlin  7832  axapti  7835  axsuploc  7837  reapval  8338  reapti  8341  reapmul1lem  8356  reapmul1  8357  reapadd1  8358  reapneg  8359  reapcotr  8360  remulext1  8361  apreim  8365  apsym  8368  apcotr  8369  apadd1  8370  addext  8372  apneg  8373  nn1m1nn  8738  nn1gt1  8754  elznn0  9069  elz2  9122  nn0n0n1ge2b  9130  nneoor  9153  uztric  9347  ltxr  9562  fzsplit2  9830  uzsplit  9872  fzospliti  9953  fzouzsplit  9956  exbtwnzlemstep  10025  exbtwnzlemex  10027  qavgle  10036  frec2uzled  10202  sq11ap  10458  sqrt11ap  10810  abs00ap  10834  maxclpr  10994  minmax  11001  minclpr  11008  xrmaxiflemcom  11018  xrminmax  11034  xrminltinf  11041  sumeq1  11124  sumeq2  11128  fz1f1o  11144  summodc  11152  fsum3  11156  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  prodmodc  11347  zeo3  11565  odd2np1lem  11569  dvdsprime  11803  coprm  11822  ennnfonelemrnh  11929  reopnap  12707  decidi  13002  bj-nn0suc0  13148  bj-inf2vnlem2  13169  bj-nn0sucALT  13176  isomninnlem  13225  trilpolemlt1  13234