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  11445  sumeq2  12073  zsumdc  12099  modfsummod  12173  prodeq2  12272  zproddc  12294  mulgval  13879  mplsubgfilemcl  14984  cncnp  15225  fsumcncntop  15562  dvmptfsum  15720  dvply2g  15761  logbgcd1irrap  15965  upgriswlkdc  16485  clwwlkccatlem  16525