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  1244  ad5ant145  1271  r19.29an  2687  diffifi  7164  fimax2gtrilemstep  7171  cnegexlem3  8466  cnegex  8467  lemul12b  9152  climshftlemg  12012  prodeq2  12268  fprodmodd  12352  lcmdvds  12801  pw2dvdslemn  12887  dfgrp3mlem  13853  tgcl  15055  metss  15485  mpomulcn  15557  ivthinclemlr  15628  ivthinclemur  15630  nnnninfex  16926