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

Metamath Proof Explorer

Theorem adantl5r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis adantl5r.1 
|- ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Assertion adantl5r 
|- ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )

Proof

Step Hyp Ref Expression
1 adantl5r.1 
 |-  ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
2 1 ex 
 |-  ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ( la -> ka ) )
3 2 adantl4r 
 |-  ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) -> ( la -> ka ) )
4 3 imp 
 |-  ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )