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  4077  fnfi  7091  nninfisol  7288  swrdccatin1  11243  sumeq2  11856  zsumdc  11881  modfsummod  11955  prodeq2  12054  zproddc  12076  mulgval  13645  mplsubgfilemcl  14648  cncnp  14889  fsumcncntop  15226  dvmptfsum  15384  dvply2g  15425  logbgcd1irrap  15629