Theorem orbi12d 801

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  830  dcbid  846  ifpbi123d  1001  3orbi123d  1348  dfbi3dc  1442  eueq3dc  2981  sbcor  3077  sbcorg  3078  unjust  3204  elun  3350  elif  3621  ifbi  3630  elprg  3693  eltpg  3718  rabsnifsb  3741  rabrsndc  3743  preq12bg  3861  exmid01  4294  exmidsssnc  4299  swopolem  4408  soeq1  4418  sowlin  4423  ordtri2orexmid  4627  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  ordsoexmid  4666  ordtri2or2exmid  4675  ontri2orexmidim  4676  nn0suc  4708  nndceq0  4722  0elnn  4723  soinxp  4802  fununi  5405  funcnvuni  5406  fun11iun  5613  unpreima  5780  isosolem  5975  xporderlem  6405  poxp  6406  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  inffiexmid  7141  fidcenumlemrk  7196  isomni  7378  enomnilem  7380  finomni  7382  exmidomni  7384  fodjuomnilemres  7390  onntri45  7502  tapeq1  7514  netap  7516  2omotaplemap  7519  indpi  7605  ltexprlemloc  7870  addextpr  7884  ltsosr  8027  aptisr  8042  mulextsr1lem  8043  mulextsr1  8044  axpre-ltwlin  8146  axpre-apti  8148  axpre-mulext  8151  axltwlin  8289  axapti  8292  axsuploc  8294  reapval  8798  reapti  8801  reapmul1lem  8816  reapmul1  8817  reapadd1  8818  reapneg  8819  reapcotr  8820  remulext1  8821  apreim  8825  apsym  8828  apcotr  8829  apadd1  8830  addext  8832  apneg  8833  nn1m1nn  9203  nn1gt1  9219  elznn0  9538  elz2  9595  nn0n0n1ge2b  9603  nneoor  9626  uztric  9822  ltxr  10054  fzsplit2  10330  uzsplit  10372  nelfzo  10432  fzospliti  10458  fzouzsplit  10461  exbtwnzlemstep  10553  exbtwnzlemex  10555  qavgle  10564  frec2uzled  10737  sq11ap  11015  swrdnd  11289  sqrt11ap  11661  abs00ap  11685  maxclpr  11845  minmax  11853  minclpr  11860  xrmaxiflemcom  11872  xrminmax  11888  xrminltinf  11895  sumeq1  11978  sumeq2  11982  fz1f1o  11998  summodc  12007  fsum3  12011  prodeq1f  12176  prodeq2w  12180  prodeq2  12181  prodmodc  12202  fprodseq  12207  fprodcl2lem  12229  zeo3  12492  odd2np1lem  12496  dvdsprime  12757  coprm  12779  ennnfonelemrnh  13100  igsumvalx  13535  gsumfzval  13537  gsumpropd  13538  gsumpropd2  13539  gsumress  13541  gsum0g  13542  islring  14270  isdomn  14348  opprdomnbg  14353  znidom  14736  reopnap  15340  dich0  15446  reapef  15572  logrpap0b  15670  wilthlem1  15777  perfectlem2  15797  lgslem1  15802  upgrm  16024  upgr1or2  16025  upgr1elem1  16044  edgupgren  16065  usgruspgrben  16110  subupgr  16197  konigsberglem1  16412  decidi  16496  bj-nn0suc0  16649  bj-inf2vnlem2  16670  bj-nn0sucALT  16677  isomninnlem  16745  trilpolemlt1  16756  trirec0  16759