Theorem a2and

Description: Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019) (Proof shortened by Wolf Lammen, 19-Jan-2020)

	Ref	Expression
Hypotheses	a2and.1	|- ( ph -> ( ( ps /\ rh ) -> ( ta -> th ) ) )
	a2and.2	|- ( ph -> ( ( ps /\ rh ) -> ch ) )
Assertion	a2and	|- ( ph -> ( ( ( ps /\ ch ) -> ta ) -> ( ( ps /\ rh ) -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		a2and.1	|- ( ph -> ( ( ps /\ rh ) -> ( ta -> th ) ) )
2		a2and.2	|- ( ph -> ( ( ps /\ rh ) -> ch ) )
3	2	expd	|- ( ph -> ( ps -> ( rh -> ch ) ) )
4	3	imdistand	|- ( ph -> ( ( ps /\ rh ) -> ( ps /\ ch ) ) )
5		imim1	|- ( ( ( ps /\ ch ) -> ta ) -> ( ( ta -> th ) -> ( ( ps /\ ch ) -> th ) ) )
6	5	com3l	|- ( ( ta -> th ) -> ( ( ps /\ ch ) -> ( ( ( ps /\ ch ) -> ta ) -> th ) ) )
7	1 4 6	syl6c	|- ( ph -> ( ( ps /\ rh ) -> ( ( ( ps /\ ch ) -> ta ) -> th ) ) )
8	7	com23	|- ( ph -> ( ( ( ps /\ ch ) -> ta ) -> ( ( ps /\ rh ) -> th ) ) )