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  7198  fimax2gtrilemstep  7205  cnegexlem3  8505  cnegex  8506  lemul12b  9194  climshftlemg  12087  prodeq2  12343  fprodmodd  12427  lcmdvds  12876  pwbdvdslemn  12963  dfgrp3mlem  13956  tgcl  15256  metss  15686  mpomulcn  15758  ivthinclemlr  15829  ivthinclemur  15831  nnnninfex  17231