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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  simpl1l  1079  simpr1l  1085  simp11l  1139  simp21l  1145  simp31l  1151  en2lp  4696  tfisi  4729  funprg  5426  nnsucsssuc  6755  ecopovtrn  6896  ecopovtrng  6899  addassnqg  7739  distrnqg  7744  ltsonq  7755  ltanqg  7757  ltmnqg  7758  distrnq0  7816  addassnq0  7819  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1lem  8137  mulextsr1  8138  axmulass  8230  axdistr  8231  dmdcanap  9042  lt2msq1  9205  ltdiv2  9207  lediv2  9211  xaddass  10250  xaddass2  10251  xlt2add  10261  modqdi  10807  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  swrdspsleq  11417  pfxeq  11446  ccatopth2  11467  pfxccat3  11484  resqrtcl  11773  bdtrilem  11983  bdtri  11984  xrbdtri  12020  bitsfzo  12700  prmexpb  12907  4sqlem18  13165  subgabl  14113  rng1zrlem  14233  opprringbg  14358  cnptoprest  15263  ssblps  15449  ssbl  15450  plyadd  15775  plymul  15776  rplogbchbase  15975  rplogbreexp  15978  relogbcxpbap  15990  lgssq  16073  uhgr2edg  16361  clwwlkccat  16556