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  2977  sbcor  3073  sbcorg  3074  unjust  3200  elun  3345  elif  3614  ifbi  3623  elprg  3686  eltpg  3711  rabrsndc  3734  preq12bg  3851  exmid01  4283  exmidsssnc  4288  swopolem  4397  soeq1  4407  sowlin  4412  ordtri2orexmid  4616  regexmidlemm  4625  regexmidlem1  4626  reg2exmidlema  4627  ordsoexmid  4655  ordtri2or2exmid  4664  ontri2orexmidim  4665  nn0suc  4697  nndceq0  4711  0elnn  4712  soinxp  4791  fununi  5392  funcnvuni  5393  fun11iun  5598  unpreima  5765  isosolem  5957  xporderlem  6388  poxp  6389  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecsuc  6564  inffiexmid  7084  fidcenumlemrk  7137  isomni  7319  enomnilem  7321  finomni  7323  exmidomni  7325  fodjuomnilemres  7331  onntri45  7442  tapeq1  7454  netap  7456  2omotaplemap  7459  indpi  7545  ltexprlemloc  7810  addextpr  7824  ltsosr  7967  aptisr  7982  mulextsr1lem  7983  mulextsr1  7984  axpre-ltwlin  8086  axpre-apti  8088  axpre-mulext  8091  axltwlin  8230  axapti  8233  axsuploc  8235  reapval  8739  reapti  8742  reapmul1lem  8757  reapmul1  8758  reapadd1  8759  reapneg  8760  reapcotr  8761  remulext1  8762  apreim  8766  apsym  8769  apcotr  8770  apadd1  8771  addext  8773  apneg  8774  nn1m1nn  9144  nn1gt1  9160  elznn0  9477  elz2  9534  nn0n0n1ge2b  9542  nneoor  9565  uztric  9761  ltxr  9988  fzsplit2  10263  uzsplit  10305  nelfzo  10365  fzospliti  10391  fzouzsplit  10394  exbtwnzlemstep  10484  exbtwnzlemex  10486  qavgle  10495  frec2uzled  10668  sq11ap  10946  swrdnd  11212  sqrt11ap  11570  abs00ap  11594  maxclpr  11754  minmax  11762  minclpr  11769  xrmaxiflemcom  11781  xrminmax  11797  xrminltinf  11804  sumeq1  11887  sumeq2  11891  fz1f1o  11907  summodc  11915  fsum3  11919  prodeq1f  12084  prodeq2w  12088  prodeq2  12089  prodmodc  12110  fprodseq  12115  fprodcl2lem  12137  zeo3  12400  odd2np1lem  12404  dvdsprime  12665  coprm  12687  ennnfonelemrnh  13008  igsumvalx  13443  gsumfzval  13445  gsumpropd  13446  gsumpropd2  13447  gsumress  13449  gsum0g  13450  islring  14177  isdomn  14254  opprdomnbg  14259  znidom  14642  reopnap  15241  dich0  15347  reapef  15473  logrpap0b  15571  wilthlem1  15675  perfectlem2  15695  lgslem1  15700  upgrm  15921  upgr1or2  15922  upgr1elem1  15941  edgupgren  15960  usgruspgrben  16005  decidi  16268  bj-nn0suc0  16422  bj-inf2vnlem2  16443  bj-nn0sucALT  16450  isomninnlem  16512  trilpolemlt1  16523  trirec0  16526