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  7255  mapfi  7266  nninfisol  7480  swrdccatin1  11520  sumeq2  12151  zsumdc  12177  modfsummod  12251  prodeq2  12350  zproddc  12372  mulgval  13985  gsummptfidmsplit  14255  mplsubgfilemcl  15227  cncnp  15468  fsumcncntop  15805  dvmptfsum  15963  dvply2g  16004  logbgcd1irrap  16218  upgriswlkdc  16818  clwwlkccatlem  16858