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  2954  sbcor  3050  sbcorg  3051  unjust  3177  elun  3322  elif  3591  ifbi  3600  elprg  3663  eltpg  3688  rabrsndc  3711  preq12bg  3827  exmid01  4258  exmidsssnc  4263  swopolem  4370  soeq1  4380  sowlin  4385  ordtri2orexmid  4589  regexmidlemm  4598  regexmidlem1  4599  reg2exmidlema  4600  ordsoexmid  4628  ordtri2or2exmid  4637  ontri2orexmidim  4638  nn0suc  4670  nndceq0  4684  0elnn  4685  soinxp  4763  fununi  5361  funcnvuni  5362  fun11iun  5565  unpreima  5728  isosolem  5916  xporderlem  6340  poxp  6341  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  inffiexmid  7029  fidcenumlemrk  7082  isomni  7264  enomnilem  7266  finomni  7268  exmidomni  7270  fodjuomnilemres  7276  onntri45  7387  tapeq1  7399  netap  7401  2omotaplemap  7404  indpi  7490  ltexprlemloc  7755  addextpr  7769  ltsosr  7912  aptisr  7927  mulextsr1lem  7928  mulextsr1  7929  axpre-ltwlin  8031  axpre-apti  8033  axpre-mulext  8036  axltwlin  8175  axapti  8178  axsuploc  8180  reapval  8684  reapti  8687  reapmul1lem  8702  reapmul1  8703  reapadd1  8704  reapneg  8705  reapcotr  8706  remulext1  8707  apreim  8711  apsym  8714  apcotr  8715  apadd1  8716  addext  8718  apneg  8719  nn1m1nn  9089  nn1gt1  9105  elznn0  9422  elz2  9479  nn0n0n1ge2b  9487  nneoor  9510  uztric  9705  ltxr  9932  fzsplit2  10207  uzsplit  10249  nelfzo  10309  fzospliti  10335  fzouzsplit  10338  exbtwnzlemstep  10427  exbtwnzlemex  10429  qavgle  10438  frec2uzled  10611  sq11ap  10889  swrdnd  11150  sqrt11ap  11464  abs00ap  11488  maxclpr  11648  minmax  11656  minclpr  11663  xrmaxiflemcom  11675  xrminmax  11691  xrminltinf  11698  sumeq1  11781  sumeq2  11785  fz1f1o  11801  summodc  11809  fsum3  11813  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  prodmodc  12004  fprodseq  12009  fprodcl2lem  12031  zeo3  12294  odd2np1lem  12298  dvdsprime  12559  coprm  12581  ennnfonelemrnh  12902  igsumvalx  13336  gsumfzval  13338  gsumpropd  13339  gsumpropd2  13340  gsumress  13342  gsum0g  13343  islring  14069  isdomn  14146  opprdomnbg  14151  znidom  14534  reopnap  15133  dich0  15239  reapef  15365  logrpap0b  15463  wilthlem1  15567  perfectlem2  15587  lgslem1  15592  upgrm  15811  upgr1or2  15812  upgr1elem1  15828  edgupgren  15845  decidi  15931  bj-nn0suc0  16085  bj-inf2vnlem2  16106  bj-nn0sucALT  16113  isomninnlem  16171  trilpolemlt1  16182  trirec0  16185