Theorem orbi12d 793

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  822  dcbid  838  3orbi123d  1311  dfbi3dc  1397  eueq3dc  2913  sbcor  3009  sbcorg  3010  unjust  3134  elun  3278  ifbi  3556  elprg  3614  eltpg  3639  rabrsndc  3662  preq12bg  3775  exmid01  4200  exmidsssnc  4205  swopolem  4307  soeq1  4317  sowlin  4322  ordtri2orexmid  4524  regexmidlemm  4533  regexmidlem1  4534  reg2exmidlema  4535  ordsoexmid  4563  ordtri2or2exmid  4572  ontri2orexmidim  4573  nn0suc  4605  nndceq0  4619  0elnn  4620  soinxp  4698  fununi  5286  funcnvuni  5287  fun11iun  5484  unpreima  5643  isosolem  5827  xporderlem  6234  poxp  6235  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  inffiexmid  6908  fidcenumlemrk  6955  isomni  7136  enomnilem  7138  finomni  7140  exmidomni  7142  fodjuomnilemres  7148  onntri45  7242  tapeq1  7253  netap  7255  2omotaplemap  7258  indpi  7343  ltexprlemloc  7608  addextpr  7622  ltsosr  7765  aptisr  7780  mulextsr1lem  7781  mulextsr1  7782  axpre-ltwlin  7884  axpre-apti  7886  axpre-mulext  7889  axltwlin  8027  axapti  8030  axsuploc  8032  reapval  8535  reapti  8538  reapmul1lem  8553  reapmul1  8554  reapadd1  8555  reapneg  8556  reapcotr  8557  remulext1  8558  apreim  8562  apsym  8565  apcotr  8566  apadd1  8567  addext  8569  apneg  8570  nn1m1nn  8939  nn1gt1  8955  elznn0  9270  elz2  9326  nn0n0n1ge2b  9334  nneoor  9357  uztric  9551  ltxr  9777  fzsplit2  10052  uzsplit  10094  fzospliti  10178  fzouzsplit  10181  exbtwnzlemstep  10250  exbtwnzlemex  10252  qavgle  10261  frec2uzled  10431  sq11ap  10690  sqrt11ap  11049  abs00ap  11073  maxclpr  11233  minmax  11240  minclpr  11247  xrmaxiflemcom  11259  xrminmax  11275  xrminltinf  11282  sumeq1  11365  sumeq2  11369  fz1f1o  11385  summodc  11393  fsum3  11397  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  prodmodc  11588  fprodseq  11593  fprodcl2lem  11615  zeo3  11875  odd2np1lem  11879  dvdsprime  12124  coprm  12146  ennnfonelemrnh  12419  islring  13338  reopnap  14077  reapef  14238  logrpap0b  14336  lgslem1  14440  decidi  14586  bj-nn0suc0  14741  bj-inf2vnlem2  14762  bj-nn0sucALT  14769  isomninnlem  14817  trilpolemlt1  14828  trirec0  14831