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  5964  xporderlem  6395  poxp  6396  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  inffiexmid  7097  fidcenumlemrk  7152  isomni  7334  enomnilem  7336  finomni  7338  exmidomni  7340  fodjuomnilemres  7346  onntri45  7458  tapeq1  7470  netap  7472  2omotaplemap  7475  indpi  7561  ltexprlemloc  7826  addextpr  7840  ltsosr  7983  aptisr  7998  mulextsr1lem  7999  mulextsr1  8000  axpre-ltwlin  8102  axpre-apti  8104  axpre-mulext  8107  axltwlin  8246  axapti  8249  axsuploc  8251  reapval  8755  reapti  8758  reapmul1lem  8773  reapmul1  8774  reapadd1  8775  reapneg  8776  reapcotr  8777  remulext1  8778  apreim  8782  apsym  8785  apcotr  8786  apadd1  8787  addext  8789  apneg  8790  nn1m1nn  9160  nn1gt1  9176  elznn0  9493  elz2  9550  nn0n0n1ge2b  9558  nneoor  9581  uztric  9777  ltxr  10009  fzsplit2  10284  uzsplit  10326  nelfzo  10386  fzospliti  10412  fzouzsplit  10415  exbtwnzlemstep  10506  exbtwnzlemex  10508  qavgle  10517  frec2uzled  10690  sq11ap  10968  swrdnd  11239  sqrt11ap  11598  abs00ap  11622  maxclpr  11782  minmax  11790  minclpr  11797  xrmaxiflemcom  11809  xrminmax  11825  xrminltinf  11832  sumeq1  11915  sumeq2  11919  fz1f1o  11935  summodc  11943  fsum3  11947  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  prodmodc  12138  fprodseq  12143  fprodcl2lem  12165  zeo3  12428  odd2np1lem  12432  dvdsprime  12693  coprm  12715  ennnfonelemrnh  13036  igsumvalx  13471  gsumfzval  13473  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  gsum0g  13478  islring  14205  isdomn  14282  opprdomnbg  14287  znidom  14670  reopnap  15269  dich0  15375  reapef  15501  logrpap0b  15599  wilthlem1  15703  perfectlem2  15723  lgslem1  15728  upgrm  15950  upgr1or2  15951  upgr1elem1  15970  edgupgren  15991  usgruspgrben  16036  subupgr  16123  decidi  16391  bj-nn0suc0  16545  bj-inf2vnlem2  16566  bj-nn0sucALT  16573  isomninnlem  16634  trilpolemlt1  16645  trirec0  16648