Theorem adantllr 473

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
adantllr	|- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ph /\ ta ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 400	1 |- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4ant13  505  ad4ant134  1207  r19.29an  2608  diffifi  6860  fimax2gtrilemstep  6866  cnegexlem3  8075  cnegex  8076  lemul12b  8756  climshftlemg  11243  prodeq2  11498  fprodmodd  11582  lcmdvds  12011  pw2dvdslemn  12097  tgcl  12704  metss  13134  ivthinclemlr  13255  ivthinclemur  13257