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  7250  mapfi  7261  nninfisol  7473  swrdccatin1  11497  sumeq2  12125  zsumdc  12151  modfsummod  12225  prodeq2  12324  zproddc  12346  mulgval  13925  mplsubgfilemcl  15090  cncnp  15331  fsumcncntop  15668  dvmptfsum  15826  dvply2g  15867  logbgcd1irrap  16076  upgriswlkdc  16605  clwwlkccatlem  16645