Theorem sbc3or

Description: sbcor with a 3-disjuncts. This proof is sbc3orgVD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Revised by NM, 24-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbc3or	|- ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) )

Proof

Step	Hyp	Ref	Expression
1		sbcor	|- ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) )
2		df-3or	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
3	2	bicomi	|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) )
4	3	sbcbii	|- ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) )
5		sbcor	|- ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) )
6	5	orbi1i	|- ( ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) )
7	1 4 6	3bitr3i	|- ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) )
8		df-3or	|- ( ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) )
9	7 8	bitr4i	|- ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) )