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  4109  fnfi  7216  mapfi  7227  nninfisol  7437  swrdccatin1  11442  sumeq2  12069  zsumdc  12095  modfsummod  12169  prodeq2  12268  zproddc  12290  mulgval  13923  mplsubgfilemcl  14966  cncnp  15207  fsumcncntop  15544  dvmptfsum  15702  dvply2g  15743  logbgcd1irrap  15947  upgriswlkdc  16467  clwwlkccatlem  16507