Theorem simp1l 1048

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 1045	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

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

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 1007

This theorem is referenced by:  simpl1l  1075  simpr1l  1081  simp11l  1135  simp21l  1141  simp31l  1147  en2lp  4676  tfisi  4709  funprg  5406  nnsucsssuc  6725  ecopovtrn  6866  ecopovtrng  6869  addassnqg  7697  distrnqg  7702  ltsonq  7713  ltanqg  7715  ltmnqg  7716  distrnq0  7774  addassnq0  7777  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1lem  8095  mulextsr1  8096  axmulass  8188  axdistr  8189  dmdcanap  8996  lt2msq1  9159  ltdiv2  9161  lediv2  9165  xaddass  10202  xaddass2  10203  xlt2add  10213  modqdi  10754  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  swrdspsleq  11359  pfxeq  11388  ccatopth2  11409  pfxccat3  11426  resqrtcl  11714  bdtrilem  11924  bdtri  11925  xrbdtri  11961  bitsfzo  12641  prmexpb  12848  4sqlem18  13106  subgabl  14049  opprringbg  14224  cnptoprest  15104  ssblps  15290  ssbl  15291  plyadd  15616  plymul  15617  rplogbchbase  15815  rplogbreexp  15818  relogbcxpbap  15830  lgssq  15913  uhgr2edg  16201  clwwlkccat  16396