Theorem simp-4l 541

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 533	. 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  543  disjiun  4078  fnfi  7114  nninfisol  7311  swrdccatin1  11273  sumeq2  11886  zsumdc  11911  modfsummod  11985  prodeq2  12084  zproddc  12106  mulgval  13675  mplsubgfilemcl  14679  cncnp  14920  fsumcncntop  15257  dvmptfsum  15415  dvply2g  15456  logbgcd1irrap  15660  upgriswlkdc  16106  clwwlkccatlem  16143