Theorem orbi12d 707

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

Syntax hints:   → wi 4   ↔ wb 98   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.39  735  dcbid  748  3orbi123d  1206  dfbi3dc  1288  eueq3dc  2715  sbcor  2807  sbcorg  2808  unjust  2921  elun  3084  ifbi  3348  elprg  3395  eltpg  3416  rabrsndc  3438  preq12bg  3544  swopolem  4042  soeq1  4052  sowlin  4057  ordtri2orexmid  4248  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  ordsoexmid  4286  ordtri2or2exmid  4296  nn0suc  4327  nndceq0  4339  0elnn  4340  soinxp  4410  fununi  4967  funcnvuni  4968  fun11iun  5147  unpreima  5292  isosolem  5463  xporderlem  5852  poxp  5853  frec0g  5983  frecsuclem3  5990  frecsuc  5991  indpi  6438  ltexprlemloc  6703  addextpr  6717  ltsosr  6847  aptisr  6861  mulextsr1lem  6862  mulextsr1  6863  axpre-ltwlin  6955  axpre-apti  6957  axpre-mulext  6960  axltwlin  7085  axapti  7088  reapval  7565  reapti  7568  reapmul1lem  7583  reapmul1  7584  reapadd1  7585  reapneg  7586  reapcotr  7587  remulext1  7588  apreim  7592  apsym  7595  apcotr  7596  apadd1  7597  addext  7599  apneg  7600  nn1m1nn  7930  nn1gt1  7945  elznn0  8258  elz2  8310  nn0n0n1ge2b  8318  nneoor  8338  uztric  8492  ltxr  8693  fzsplit2  8912  uzsplit  8952  fzospliti  9030  fzouzsplit  9033  sq11ap  9412  sqrt11ap  9634  abs00ap  9658  sumeq1  9872  bj-dcbi  10046  bj-nn0suc0  10073  bj-inf2vnlem2  10094  bj-nn0sucALT  10101