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  4083  fnfi  7135  nninfisol  7332  swrdccatin1  11310  sumeq2  11924  zsumdc  11950  modfsummod  12024  prodeq2  12123  zproddc  12145  mulgval  13714  mplsubgfilemcl  14719  cncnp  14960  fsumcncntop  15297  dvmptfsum  15455  dvply2g  15496  logbgcd1irrap  15700  upgriswlkdc  16217  clwwlkccatlem  16257