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  7202  fimax2gtrilemstep  7209  cnegexlem3  8510  cnegex  8511  lemul12b  9199  climshftlemg  12093  prodeq2  12349  fprodmodd  12433  lcmdvds  12882  pwbdvdslemn  12969  dfgrp3mlem  13962  tgcl  15290  metss  15720  mpomulcn  15792  ivthinclemlr  15863  ivthinclemur  15865  nnnninfex  17271