This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )