Theorem adantllr 481

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 109	. 2 |- ( ( ph /\ ta ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 402	1 |- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad4ant13  513  ad4ant134  1220  ad5ant145  1247  r19.29an  2650  diffifi  7017  fimax2gtrilemstep  7023  cnegexlem3  8284  cnegex  8285  lemul12b  8969  climshftlemg  11728  prodeq2  11983  fprodmodd  12067  lcmdvds  12516  pw2dvdslemn  12602  dfgrp3mlem  13545  tgcl  14651  metss  15081  mpomulcn  15153  ivthinclemlr  15224  ivthinclemur  15226  nnnninfex  16161