Theorem 3impcombi

Description: A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017)

	Ref	Expression
Hypothesis	3impcombi.1	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜑 ) → ( 𝜒 ↔ 𝜃 ) )
Assertion	3impcombi	⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		3impcombi.1	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜑 ) → ( 𝜒 ↔ 𝜃 ) )
2	1	biimpd	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜑 ) → ( 𝜒 → 𝜃 ) )
3	2	3anidm13	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) )
4	3	ancoms	⊢ ( ( 𝜓 ∧ 𝜑 ) → ( 𝜒 → 𝜃 ) )
5	4	3impia	⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜃 )