Theorem orbi12d 706

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 704	. 2 ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ θ)))
3		orbi12d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	orbi2d 703	. 2 ⊢ (φ → ((χ ∨ θ) ↔ (χ ∨ τ)))
5	2, 4	bitrd 177	1 ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ τ)))

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

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 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.39  734  dcbid  747  3orbi123d  1205  dfbi3dc  1285  eueq3dc  2709  sbcor  2801  sbcorg  2802  unjust  2915  elun  3078  ifbi  3342  elprg  3384  eltpg  3407  rabrsndc  3429  preq12bg  3535  swopolem  4033  soeq1  4043  sowlin  4048  ordtri2orexmid  4211  regexmidlemm  4217  regexmidlem1  4218  ordsoexmid  4240  nn0suc  4270  nndceq0  4282  0elnn  4283  soinxp  4353  fununi  4910  funcnvuni  4911  fun11iun  5090  unpreima  5235  isosolem  5406  xporderlem  5793  poxp  5794  frec0g  5922  frecsuclem3  5929  frecsuc  5930  indpi  6326  ltexprlemloc  6580  addextpr  6592  ltsosr  6672  aptisr  6685  mulextsr1lem  6686  mulextsr1  6687  axpre-ltwlin  6747  axpre-apti  6749  axpre-mulext  6752  axltwlin  6864  axapti  6867  reapval  7340  reapti  7343  reapmul1lem  7358  reapmul1  7359  reapadd1  7360  reapneg  7361  reapcotr  7362  remulext1  7363  apreim  7367  apsym  7370  apcotr  7371  apadd1  7372  addext  7374  apneg  7375  nn1m1nn  7693  nn1gt1  7708  elznn0  8016  elz2  8068  nn0n0n1ge2b  8076  nneoor  8096  uztric  8250  ltxr  8445  fzsplit2  8664  uzsplit  8704  fzospliti  8782  fzouzsplit  8785  bj-dcbi  9359  bj-nn0suc0  9384  bj-inf2vnlem2  9401  bj-nn0sucALT  9408