Theorem ad4antlr 732

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

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  ad5antlr  734  restcld  18781  pthaus  19216  txhaus  19225  xkohaus  19231  alexsubALTlem4  19627  ustuqtop3  19823  ulmcau  21865  pstmxmet  26329  heicant  28431  mblfinlem3  28435  mblfinlem4  28436  itg2addnclem2  28449  itg2gt0cn  28452  ftc1cnnc  28471  nn0prpwlem  28522  sstotbnd2  28678  jm2.26lem3  29355  usgra2wlkspth  30303  clwlkisclwwlklem1  30454  usg2spot2nb  30663  ply1mulgsumlem2  30850  pmatcollpw1dst  30906