Theorem ad4antlr 744

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

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad4antlr	|- ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) -> ps )

Proof of Theorem ad4antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad3antlr 742	. 2 |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )
3	2	adantr 471	1 |- ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  ad5antlr  746  initoeu2  15959  cpmatacl  19788  cpmatmcllem  19790  cpmatmcl  19791  chfacfisf  19926  chfacfisfcpmat  19927  restcld  20236  pthaus  20701  txhaus  20710  xkohaus  20716  alexsubALTlem4  21113  ustuqtop3  21306  ulmcau  23398  usgra2wlkspth  25397  clwlkisclwwlklem1  25563  usg2spot2nb  25841  locfinreflem  28715  cmpcref  28725  pstmxmet  28748  sigapildsys  29032  ldgenpisyslem1  29033  nn0prpwlem  31026  poimirlem29  32013  heicant  32019  mblfinlem3  32023  mblfinlem4  32024  itg2addnclem2  32038  itg2gt0cn  32041  ftc1cnnc  32060  sstotbnd2  32150  pell1234qrdich  35751  jm2.26lem3  35900  cvgdvgrat  36705  icccncfext  37802  fourierdlem34  38041  fourierdlem87  38094  etransclem35  38171  bgoldbwt  38915  bgoldbtbnd  38941  ply1mulgsumlem2  40451  nn0sumshdiglemA  40702