Theorem 3orbi123d 1345

Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	|- ( ph -> ( ps <-> ch ) )
bi3d.2	|- ( ph -> ( th <-> ta ) )
bi3d.3	|- ( ph -> ( et <-> ze ) )

Assertion

Ref	Expression
3orbi123d	|- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )

Proof of Theorem 3orbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2		bi3d.2	. . . 4 |- ( ph -> ( th <-> ta ) )
3	1, 2	orbi12d 798	. . 3 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	orbi12d 798	. 2 |- ( ph -> ( ( ( ps \/ th ) \/ et ) <-> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or 1003	. 2 |- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or 1003	. 2 |- ( ( ch \/ ta \/ ze ) <-> ( ( ch \/ ta ) \/ ze ) )
8	5, 6, 7	3bitr4g 223	1 |- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 713   \/ w3o 1001

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 714

This theorem depends on definitions:  df-bi 117  df-3or 1003

This theorem is referenced by:  ordtriexmid  4613  ontriexmidim  4614  wetriext  4669  nntri3or  6647  tridc  7070  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  onntri35  7433  ltsopi  7518  pitri3or  7520  nqtri3or  7594  elz  9459  ztri3or  9500  qtri3or  10472  trilpo  16499  trirec0  16500  reap0  16514