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  1219  ad5ant145  1246  r19.29an  2639  diffifi  6955  fimax2gtrilemstep  6961  cnegexlem3  8203  cnegex  8204  lemul12b  8888  climshftlemg  11467  prodeq2  11722  fprodmodd  11806  lcmdvds  12247  pw2dvdslemn  12333  dfgrp3mlem  13230  tgcl  14300  metss  14730  mpomulcn  14802  ivthinclemlr  14873  ivthinclemur  14875