Theorem orbi12d 798

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
orbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
orbi12d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		orbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi1d 796	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		orbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 795	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

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  2978  sbcor  3074  sbcorg  3075  unjust  3201  elun  3346  elif  3615  ifbi  3624  elprg  3687  eltpg  3712  rabsnifsb  3735  rabrsndc  3737  preq12bg  3854  exmid01  4286  exmidsssnc  4291  swopolem  4400  soeq1  4410  sowlin  4415  ordtri2orexmid  4619  regexmidlemm  4628  regexmidlem1  4629  reg2exmidlema  4630  ordsoexmid  4658  ordtri2or2exmid  4667  ontri2orexmidim  4668  nn0suc  4700  nndceq0  4714  0elnn  4715  soinxp  4794  fununi  5395  funcnvuni  5396  fun11iun  5601  unpreima  5768  isosolem  5960  xporderlem  6391  poxp  6392  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  inffiexmid  7091  fidcenumlemrk  7144  isomni  7326  enomnilem  7328  finomni  7330  exmidomni  7332  fodjuomnilemres  7338  onntri45  7449  tapeq1  7461  netap  7463  2omotaplemap  7466  indpi  7552  ltexprlemloc  7817  addextpr  7831  ltsosr  7974  aptisr  7989  mulextsr1lem  7990  mulextsr1  7991  axpre-ltwlin  8093  axpre-apti  8095  axpre-mulext  8098  axltwlin  8237  axapti  8240  axsuploc  8242  reapval  8746  reapti  8749  reapmul1lem  8764  reapmul1  8765  reapadd1  8766  reapneg  8767  reapcotr  8768  remulext1  8769  apreim  8773  apsym  8776  apcotr  8777  apadd1  8778  addext  8780  apneg  8781  nn1m1nn  9151  nn1gt1  9167  elznn0  9484  elz2  9541  nn0n0n1ge2b  9549  nneoor  9572  uztric  9768  ltxr  10000  fzsplit2  10275  uzsplit  10317  nelfzo  10377  fzospliti  10403  fzouzsplit  10406  exbtwnzlemstep  10497  exbtwnzlemex  10499  qavgle  10508  frec2uzled  10681  sq11ap  10959  swrdnd  11230  sqrt11ap  11589  abs00ap  11613  maxclpr  11773  minmax  11781  minclpr  11788  xrmaxiflemcom  11800  xrminmax  11816  xrminltinf  11823  sumeq1  11906  sumeq2  11910  fz1f1o  11926  summodc  11934  fsum3  11938  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  prodmodc  12129  fprodseq  12134  fprodcl2lem  12156  zeo3  12419  odd2np1lem  12423  dvdsprime  12684  coprm  12706  ennnfonelemrnh  13027  igsumvalx  13462  gsumfzval  13464  gsumpropd  13465  gsumpropd2  13466  gsumress  13468  gsum0g  13469  islring  14196  isdomn  14273  opprdomnbg  14278  znidom  14661  reopnap  15260  dich0  15366  reapef  15492  logrpap0b  15590  wilthlem1  15694  perfectlem2  15714  lgslem1  15719  upgrm  15941  upgr1or2  15942  upgr1elem1  15961  edgupgren  15980  usgruspgrben  16025  decidi  16327  bj-nn0suc0  16481  bj-inf2vnlem2  16502  bj-nn0sucALT  16509  isomninnlem  16570  trilpolemlt1  16581  trirec0  16584