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

Metamath Proof Explorer

Theorem pm2.61ddan

Description: Elimination of two antecedents. (Contributed by NM, 9-Jul-2013)

Ref Expression
Hypotheses pm2.61ddan.1 
|- ( ( ph /\ ps ) -> th )
pm2.61ddan.2 
|- ( ( ph /\ ch ) -> th )
pm2.61ddan.3 
|- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )
Assertion pm2.61ddan 
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 pm2.61ddan.1 
 |-  ( ( ph /\ ps ) -> th )
2 pm2.61ddan.2 
 |-  ( ( ph /\ ch ) -> th )
3 pm2.61ddan.3 
 |-  ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )
4 2 adantlr 
 |-  ( ( ( ph /\ -. ps ) /\ ch ) -> th )
5 3 anassrs 
 |-  ( ( ( ph /\ -. ps ) /\ -. ch ) -> th )
6 4 5 pm2.61dan 
 |-  ( ( ph /\ -. ps ) -> th )
7 1 6 pm2.61dan 
 |-  ( ph -> th )