Theorem 3orbi123 38717

Description: pm4.39 915 with a 3-conjunct antecedent. This proof is 3orbi123VD 39085 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem 3orbi123

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ph <-> ps ) )
2		simp2 1062	. 2 |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ch <-> th ) )
3		simp3 1063	. 2 |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ta <-> et ) )
4	1, 2, 3	3orbi123d 1398	1 |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ w3o 1036   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039

This theorem is referenced by:  sbcoreleleq  38745  sbcoreleleqVD  39095