Description: Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bi2an9.1 | ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) | |
bi2an9.2 | ⊢ ( 𝜃 → ( 𝜏 ↔ 𝜂 ) ) | ||
Assertion | bi2bian9 | ⊢ ( ( 𝜑 ∧ 𝜃 ) → ( ( 𝜓 ↔ 𝜏 ) ↔ ( 𝜒 ↔ 𝜂 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2an9.1 | ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) | |
2 | bi2an9.2 | ⊢ ( 𝜃 → ( 𝜏 ↔ 𝜂 ) ) | |
3 | 1 | adantr | ⊢ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜓 ↔ 𝜒 ) ) |
4 | 2 | adantl | ⊢ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜏 ↔ 𝜂 ) ) |
5 | 3 4 | bibi12d | ⊢ ( ( 𝜑 ∧ 𝜃 ) → ( ( 𝜓 ↔ 𝜏 ) ↔ ( 𝜒 ↔ 𝜂 ) ) ) |