Theorem simp-4l 547

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 539	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )
2	1	adantr 276	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-5l  549  disjiun  4125  fnfi  7256  mapfi  7267  nninfisol  7480  swrdccatin1  11519  sumeq2  12150  zsumdc  12176  modfsummod  12250  prodeq2  12349  zproddc  12371  mulgval  13984  gsummptfidmsplit  14254  cncnp  15489  fsumcncntop  15826  dvmptfsum  15984  dvply2g  16025  logbgcd1irrap  16239  upgriswlkdc  16839  clwwlkccatlem  16879