Theorem adantllr 485

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 406	1 |- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4ant13  517  ad4ant134  1248  ad5ant145  1275  r19.29an  2693  diffifi  7204  fimax2gtrilemstep  7211  cnegexlem3  8510  cnegex  8511  lemul12b  9199  climshftlemg  12092  prodeq2  12348  fprodmodd  12432  lcmdvds  12881  pwbdvdslemn  12968  dfgrp3mlem  13961  tgcl  15307  metss  15737  mpomulcn  15809  ivthinclemlr  15880  ivthinclemur  15882  nnnninfex  17288