Theorem orbi12d 795

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  824  dcbid  840  3orbi123d  1324  dfbi3dc  1417  eueq3dc  2947  sbcor  3043  sbcorg  3044  unjust  3169  elun  3314  ifbi  3591  elprg  3653  eltpg  3678  rabrsndc  3701  preq12bg  3814  exmid01  4242  exmidsssnc  4247  swopolem  4352  soeq1  4362  sowlin  4367  ordtri2orexmid  4571  regexmidlemm  4580  regexmidlem1  4581  reg2exmidlema  4582  ordsoexmid  4610  ordtri2or2exmid  4619  ontri2orexmidim  4620  nn0suc  4652  nndceq0  4666  0elnn  4667  soinxp  4745  fununi  5342  funcnvuni  5343  fun11iun  5543  unpreima  5705  isosolem  5893  xporderlem  6317  poxp  6318  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  inffiexmid  7003  fidcenumlemrk  7056  isomni  7238  enomnilem  7240  finomni  7242  exmidomni  7244  fodjuomnilemres  7250  onntri45  7353  tapeq1  7364  netap  7366  2omotaplemap  7369  indpi  7455  ltexprlemloc  7720  addextpr  7734  ltsosr  7877  aptisr  7892  mulextsr1lem  7893  mulextsr1  7894  axpre-ltwlin  7996  axpre-apti  7998  axpre-mulext  8001  axltwlin  8140  axapti  8143  axsuploc  8145  reapval  8649  reapti  8652  reapmul1lem  8667  reapmul1  8668  reapadd1  8669  reapneg  8670  reapcotr  8671  remulext1  8672  apreim  8676  apsym  8679  apcotr  8680  apadd1  8681  addext  8683  apneg  8684  nn1m1nn  9054  nn1gt1  9070  elznn0  9387  elz2  9444  nn0n0n1ge2b  9452  nneoor  9475  uztric  9670  ltxr  9897  fzsplit2  10172  uzsplit  10214  nelfzo  10274  fzospliti  10300  fzouzsplit  10303  exbtwnzlemstep  10390  exbtwnzlemex  10392  qavgle  10401  frec2uzled  10574  sq11ap  10852  swrdnd  11112  sqrt11ap  11349  abs00ap  11373  maxclpr  11533  minmax  11541  minclpr  11548  xrmaxiflemcom  11560  xrminmax  11576  xrminltinf  11583  sumeq1  11666  sumeq2  11670  fz1f1o  11686  summodc  11694  fsum3  11698  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  prodmodc  11889  fprodseq  11894  fprodcl2lem  11916  zeo3  12179  odd2np1lem  12183  dvdsprime  12444  coprm  12466  ennnfonelemrnh  12787  igsumvalx  13221  gsumfzval  13223  gsumpropd  13224  gsumpropd2  13225  gsumress  13227  gsum0g  13228  islring  13954  isdomn  14031  opprdomnbg  14036  znidom  14419  reopnap  15018  dich0  15124  reapef  15250  logrpap0b  15348  wilthlem1  15452  perfectlem2  15472  lgslem1  15477  decidi  15731  bj-nn0suc0  15886  bj-inf2vnlem2  15907  bj-nn0sucALT  15914  isomninnlem  15969  trilpolemlt1  15980  trirec0  15983