Theorem simp-4l 543

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4l	|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		simplll 535	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
2	1	adantr 276	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp-5l  545  disjiun  4088  fnfi  7178  nninfisol  7375  swrdccatin1  11353  sumeq2  11980  zsumdc  12006  modfsummod  12080  prodeq2  12179  zproddc  12201  mulgval  13770  mplsubgfilemcl  14780  cncnp  15021  fsumcncntop  15358  dvmptfsum  15516  dvply2g  15557  logbgcd1irrap  15761  upgriswlkdc  16281  clwwlkccatlem  16321