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  2938  sbcor  3034  sbcorg  3035  unjust  3160  elun  3305  ifbi  3582  elprg  3643  eltpg  3668  rabrsndc  3691  preq12bg  3804  exmid01  4232  exmidsssnc  4237  swopolem  4341  soeq1  4351  sowlin  4356  ordtri2orexmid  4560  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  ordsoexmid  4599  ordtri2or2exmid  4608  ontri2orexmidim  4609  nn0suc  4641  nndceq0  4655  0elnn  4656  soinxp  4734  fununi  5327  funcnvuni  5328  fun11iun  5528  unpreima  5690  isosolem  5874  xporderlem  6298  poxp  6299  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  inffiexmid  6976  fidcenumlemrk  7029  isomni  7211  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  onntri45  7326  tapeq1  7337  netap  7339  2omotaplemap  7342  indpi  7428  ltexprlemloc  7693  addextpr  7707  ltsosr  7850  aptisr  7865  mulextsr1lem  7866  mulextsr1  7867  axpre-ltwlin  7969  axpre-apti  7971  axpre-mulext  7974  axltwlin  8113  axapti  8116  axsuploc  8118  reapval  8622  reapti  8625  reapmul1lem  8640  reapmul1  8641  reapadd1  8642  reapneg  8643  reapcotr  8644  remulext1  8645  apreim  8649  apsym  8652  apcotr  8653  apadd1  8654  addext  8656  apneg  8657  nn1m1nn  9027  nn1gt1  9043  elznn0  9360  elz2  9416  nn0n0n1ge2b  9424  nneoor  9447  uztric  9642  ltxr  9869  fzsplit2  10144  uzsplit  10186  nelfzo  10246  fzospliti  10271  fzouzsplit  10274  exbtwnzlemstep  10356  exbtwnzlemex  10358  qavgle  10367  frec2uzled  10540  sq11ap  10818  sqrt11ap  11222  abs00ap  11246  maxclpr  11406  minmax  11414  minclpr  11421  xrmaxiflemcom  11433  xrminmax  11449  xrminltinf  11456  sumeq1  11539  sumeq2  11543  fz1f1o  11559  summodc  11567  fsum3  11571  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  prodmodc  11762  fprodseq  11767  fprodcl2lem  11789  zeo3  12052  odd2np1lem  12056  dvdsprime  12317  coprm  12339  ennnfonelemrnh  12660  igsumvalx  13093  gsumfzval  13095  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  gsum0g  13100  islring  13826  isdomn  13903  opprdomnbg  13908  znidom  14291  reopnap  14890  dich0  14996  reapef  15122  logrpap0b  15220  wilthlem1  15324  perfectlem2  15344  lgslem1  15349  decidi  15549  bj-nn0suc0  15704  bj-inf2vnlem2  15725  bj-nn0sucALT  15732  isomninnlem  15787  trilpolemlt1  15798  trirec0  15801