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  4703  tfisi  4736  funprg  5434  nnsucsssuc  6770  ecopovtrn  6911  ecopovtrng  6914  addassnqg  7755  distrnqg  7760  ltsonq  7771  ltanqg  7773  ltmnqg  7774  distrnq0  7832  addassnq0  7835  mulasssrg  8131  distrsrg  8132  lttrsr  8135  ltsosr  8137  ltasrg  8143  mulextsr1lem  8153  mulextsr1  8154  axmulass  8246  axdistr  8247  dmdcanap  9060  lt2msq1  9223  ltdiv2  9225  lediv2  9229  xaddass  10287  xaddass2  10288  xlt2add  10298  modqdi  10849  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  swrdspsleq  11460  pfxeq  11489  ccatopth2  11510  pfxccat3  11527  resqrtcl  11816  bdtrilem  12029  bdtri  12030  xrbdtri  12066  bitsfzo  12746  prmexpb  12954  4sqlem18  13215  subgabl  14225  rng1zrlem  14364  opprringbg  14493  cnptoprest  15482  ssblps  15668  ssbl  15669  plyadd  15994  plymul  15995  rplogbchbase  16203  rplogbreexp  16206  relogbcxpbap  16218  lgssq  16381  uhgr2edg  16669  clwwlkccat  16864