Theorem orbi12d 794

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 792	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		orbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 791	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  823  dcbid  839  3orbi123d  1322  dfbi3dc  1408  eueq3dc  2934  sbcor  3030  sbcorg  3031  unjust  3156  elun  3300  ifbi  3577  elprg  3638  eltpg  3663  rabrsndc  3686  preq12bg  3799  exmid01  4227  exmidsssnc  4232  swopolem  4336  soeq1  4346  sowlin  4351  ordtri2orexmid  4555  regexmidlemm  4564  regexmidlem1  4565  reg2exmidlema  4566  ordsoexmid  4594  ordtri2or2exmid  4603  ontri2orexmidim  4604  nn0suc  4636  nndceq0  4650  0elnn  4651  soinxp  4729  fununi  5322  funcnvuni  5323  fun11iun  5521  unpreima  5683  isosolem  5867  xporderlem  6284  poxp  6285  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  inffiexmid  6962  fidcenumlemrk  7013  isomni  7195  enomnilem  7197  finomni  7199  exmidomni  7201  fodjuomnilemres  7207  onntri45  7301  tapeq1  7312  netap  7314  2omotaplemap  7317  indpi  7402  ltexprlemloc  7667  addextpr  7681  ltsosr  7824  aptisr  7839  mulextsr1lem  7840  mulextsr1  7841  axpre-ltwlin  7943  axpre-apti  7945  axpre-mulext  7948  axltwlin  8087  axapti  8090  axsuploc  8092  reapval  8595  reapti  8598  reapmul1lem  8613  reapmul1  8614  reapadd1  8615  reapneg  8616  reapcotr  8617  remulext1  8618  apreim  8622  apsym  8625  apcotr  8626  apadd1  8627  addext  8629  apneg  8630  nn1m1nn  9000  nn1gt1  9016  elznn0  9332  elz2  9388  nn0n0n1ge2b  9396  nneoor  9419  uztric  9614  ltxr  9841  fzsplit2  10116  uzsplit  10158  nelfzo  10218  fzospliti  10243  fzouzsplit  10246  exbtwnzlemstep  10316  exbtwnzlemex  10318  qavgle  10327  frec2uzled  10500  sq11ap  10778  sqrt11ap  11182  abs00ap  11206  maxclpr  11366  minmax  11373  minclpr  11380  xrmaxiflemcom  11392  xrminmax  11408  xrminltinf  11415  sumeq1  11498  sumeq2  11502  fz1f1o  11518  summodc  11526  fsum3  11530  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  prodmodc  11721  fprodseq  11726  fprodcl2lem  11748  zeo3  12009  odd2np1lem  12013  dvdsprime  12260  coprm  12282  ennnfonelemrnh  12573  igsumvalx  12972  gsumfzval  12974  gsumpropd  12975  gsumpropd2  12976  gsumress  12978  gsum0g  12979  islring  13688  isdomn  13765  opprdomnbg  13770  znidom  14145  reopnap  14706  dich0  14806  reapef  14913  logrpap0b  15011  wilthlem1  15112  lgslem1  15116  decidi  15287  bj-nn0suc0  15442  bj-inf2vnlem2  15463  bj-nn0sucALT  15470  isomninnlem  15520  trilpolemlt1  15531  trirec0  15534