Theorem ad4antlr 732

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

Hypothesis

Ref	Expression
ad2ant.1

Assertion

Ref	Expression
ad4antlr

Proof of Theorem ad4antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3
2	1	ad3antlr 730	. 2
3	2	adantr 465	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  ad5antlr  734  cpmatacl  19217  cpmatmcllem  19219  cpmatmcl  19220  chfacfisf  19355  chfacfisfcpmat  19356  restcld  19673  pthaus  20139  txhaus  20148  xkohaus  20154  alexsubALTlem4  20550  ustuqtop3  20746  ulmcau  22790  usgra2wlkspth  24621  clwlkisclwwlklem1  24787  usg2spot2nb  25065  locfinreflem  27843  cmpcref  27853  pstmxmet  27876  heicant  30049  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem2  30067  itg2gt0cn  30070  ftc1cnnc  30089  nn0prpwlem  30140  sstotbnd2  30270  pell1234qrdich  30797  jm2.26lem3  30943  cvgdvgrat  31194  icccncfext  31690  fourierdlem34  31923  fourierdlem87  31976  etransclem35  32052  initoeu2  32622  ply1mulgsumlem2  32987

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