Theorem orbi12d 694

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

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

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 617

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm4.39  723  dcbid  739  3orbi123d  1191  dfbi3dc  1271  eueq3dc  2692  sbcor  2784  sbcorg  2785  unjust  2898  elun  3061  ifbi  3325  elprg  3367  eltpg  3390  rabrsndc  3412  preq12bg  3518  swopolem  4016  soeq1  4026  sowlin  4031  ordtri2orexmid  4195  regexmidlemm  4201  regexmidlem1  4202  ordsoexmid  4224  nn0suc  4254  nndceq0  4266  0elnn  4267  soinxp  4337  fununi  4893  funcnvuni  4894  fun11iun  5072  unpreima  5217  isosolem  5388  xporderlem  5774  poxp  5775  frec0g  5902  frecsuclem3  5906  frecsuc  5907  ltexprlemloc  6444  ltsosr  6511  axpre-ltwlin  6577  axltwlin  6688  bj-d0clsepcl  7295  bj-nn0suc0  7319  bj-inf2vnlem2  7336  bj-nn0sucALT  7343