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  1196  r19.29an  2577  diffifi  6796  fimax2gtrilemstep  6802  cnegexlem3  7963  cnegex  7964  lemul12b  8643  climshftlemg  11103  prodeq2  11358  lcmdvds  11796  pw2dvdslemn  11879  tgcl  12272  metss  12702  ivthinclemlr  12823  ivthinclemur  12825