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  6581  addextpr  6593  ltsosr  6692  aptisr  6705  mulextsr1lem  6706  mulextsr1  6707  axpre-ltwlin  6767  axpre-apti  6769  axpre-mulext  6772  axltwlin  6884  axapti  6887  reapval  7360  reapti  7363  reapmul1lem  7378  reapmul1  7379  reapadd1  7380  reapneg  7381  reapcotr  7382  remulext1  7383  apreim  7387  apsym  7390  apcotr  7391  apadd1  7392  addext  7394  apneg  7395  nn1m1nn  7713  nn1gt1  7728  elznn0  8036  elz2  8088  nn0n0n1ge2b  8096  nneoor  8116  uztric  8270  ltxr  8465  fzsplit2  8684  uzsplit  8724  fzospliti  8802  fzouzsplit  8805  bj-dcbi  9383  bj-nn0suc0  9410  bj-inf2vnlem2  9431  bj-nn0sucALT  9438