Theorem ad4antlr 725

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 723	. 2 |- ( ( ( ( ch /\ ph ) /\ th ) /\ ta ) -> ps )
3	2	adantr 462	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  727  restcld  18617  pthaus  19052  txhaus  19061  xkohaus  19067  alexsubALTlem4  19463  ustuqtop3  19659  ulmcau  21744  pstmxmet  26177  heicant  28267  mblfinlem3  28271  mblfinlem4  28272  itg2addnclem2  28285  itg2gt0cn  28288  ftc1cnnc  28307  nn0prpwlem  28358  sstotbnd2  28514  jm2.26lem3  29192  usgra2wlkspth  30141  clwlkisclwwlklem1  30292  usg2spot2nb  30501