Theorem ad4antlr 731

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 729	. 2 |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )
3	2	adantr 463	1 |- ( ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  ad5antlr  733  initoeu2  15619  cpmatacl  19509  cpmatmcllem  19511  cpmatmcl  19512  chfacfisf  19647  chfacfisfcpmat  19648  restcld  19966  pthaus  20431  txhaus  20440  xkohaus  20446  alexsubALTlem4  20842  ustuqtop3  21038  ulmcau  23082  usgra2wlkspth  25038  clwlkisclwwlklem1  25204  usg2spot2nb  25482  locfinreflem  28296  cmpcref  28306  pstmxmet  28329  sigapildsys  28610  ldgenpisyslem1  28611  nn0prpwlem  30550  heicant  31421  mblfinlem3  31425  mblfinlem4  31426  itg2addnclem2  31440  itg2gt0cn  31443  ftc1cnnc  31462  sstotbnd2  31552  pell1234qrdich  35158  jm2.26lem3  35305  cvgdvgrat  36042  icccncfext  37058  fourierdlem34  37291  fourierdlem87  37344  etransclem35  37420  bgoldbwt  37831  bgoldbtbnd  37857  ply1mulgsumlem2  38498  nn0sumshdiglemA  38750