Theorem simp1l 1052

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	3ad2ant1 1049	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

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

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

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1l  1079  simpr1l  1085  simp11l  1139  simp21l  1145  simp31l  1151  en2lp  4701  tfisi  4734  funprg  5431  nnsucsssuc  6765  ecopovtrn  6906  ecopovtrng  6909  addassnqg  7750  distrnqg  7755  ltsonq  7766  ltanqg  7768  ltmnqg  7769  distrnq0  7827  addassnq0  7830  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  dmdcanap  9055  lt2msq1  9218  ltdiv2  9220  lediv2  9224  xaddass  10282  xaddass2  10283  xlt2add  10293  modqdi  10844  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  swrdspsleq  11455  pfxeq  11484  ccatopth2  11505  pfxccat3  11522  resqrtcl  11811  bdtrilem  12024  bdtri  12025  xrbdtri  12061  bitsfzo  12741  prmexpb  12949  4sqlem18  13210  subgabl  14220  rng1zrlem  14349  opprringbg  14476  cnptoprest  15439  ssblps  15625  ssbl  15626  plyadd  15951  plymul  15952  rplogbchbase  16160  rplogbreexp  16163  relogbcxpbap  16175  lgssq  16338  uhgr2edg  16626  clwwlkccat  16821