Description: pm4.39 with a 3-conjunct antecedent. This proof is 3orbi123VD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 3orbi123 | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ↔ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | simp2 | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( 𝜒 ↔ 𝜃 ) ) | |
| 3 | simp3 | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( 𝜏 ↔ 𝜂 ) ) | |
| 4 | 1 2 3 | 3orbi123d | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ↔ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) ) |