Theorem ad5antlr 734

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1

Assertion

Ref	Expression
ad5antlr

Proof of Theorem ad5antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3
2	1	ad4antlr 732	. 2
3	2	adantr 465	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  ad6antlr  736  restmetu  21090  usg2spot2nb  25065  foresf1o  27403  fimaproj  27836  locfinreflem  27843  pstmxmet  27876  mblfinlem3  30053  itg2gt0cn  30070  pell1234qrmulcl  30791  limclner  31657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371