Theorem orbi12d 800

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  829  dcbid  845  ifpbi123d  1000  3orbi123d  1347  dfbi3dc  1441  eueq3dc  2980  sbcor  3076  sbcorg  3077  unjust  3203  elun  3348  elif  3617  ifbi  3626  elprg  3689  eltpg  3714  rabsnifsb  3737  rabrsndc  3739  preq12bg  3856  exmid01  4288  exmidsssnc  4293  swopolem  4402  soeq1  4412  sowlin  4417  ordtri2orexmid  4621  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  ordsoexmid  4660  ordtri2or2exmid  4669  ontri2orexmidim  4670  nn0suc  4702  nndceq0  4716  0elnn  4717  soinxp  4796  fununi  5398  funcnvuni  5399  fun11iun  5604  unpreima  5772  isosolem  5965  xporderlem  6396  poxp  6397  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  inffiexmid  7098  fidcenumlemrk  7153  isomni  7335  enomnilem  7337  finomni  7339  exmidomni  7341  fodjuomnilemres  7347  onntri45  7459  tapeq1  7471  netap  7473  2omotaplemap  7476  indpi  7562  ltexprlemloc  7827  addextpr  7841  ltsosr  7984  aptisr  7999  mulextsr1lem  8000  mulextsr1  8001  axpre-ltwlin  8103  axpre-apti  8105  axpre-mulext  8108  axltwlin  8247  axapti  8250  axsuploc  8252  reapval  8756  reapti  8759  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  reapneg  8777  reapcotr  8778  remulext1  8779  apreim  8783  apsym  8786  apcotr  8787  apadd1  8788  addext  8790  apneg  8791  nn1m1nn  9161  nn1gt1  9177  elznn0  9494  elz2  9551  nn0n0n1ge2b  9559  nneoor  9582  uztric  9778  ltxr  10010  fzsplit2  10285  uzsplit  10327  nelfzo  10387  fzospliti  10413  fzouzsplit  10416  exbtwnzlemstep  10508  exbtwnzlemex  10510  qavgle  10519  frec2uzled  10692  sq11ap  10970  swrdnd  11244  sqrt11ap  11616  abs00ap  11640  maxclpr  11800  minmax  11808  minclpr  11815  xrmaxiflemcom  11827  xrminmax  11843  xrminltinf  11850  sumeq1  11933  sumeq2  11937  fz1f1o  11953  summodc  11962  fsum3  11966  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  prodmodc  12157  fprodseq  12162  fprodcl2lem  12184  zeo3  12447  odd2np1lem  12451  dvdsprime  12712  coprm  12734  ennnfonelemrnh  13055  igsumvalx  13490  gsumfzval  13492  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  gsum0g  13497  islring  14225  isdomn  14302  opprdomnbg  14307  znidom  14690  reopnap  15289  dich0  15395  reapef  15521  logrpap0b  15619  wilthlem1  15723  perfectlem2  15743  lgslem1  15748  upgrm  15970  upgr1or2  15971  upgr1elem1  15990  edgupgren  16011  usgruspgrben  16056  subupgr  16143  konigsberglem1  16358  decidi  16442  bj-nn0suc0  16596  bj-inf2vnlem2  16617  bj-nn0sucALT  16624  isomninnlem  16685  trilpolemlt1  16696  trirec0  16699