Theorem simp1l 1023

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

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

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 982

This theorem is referenced by:  simpl1l  1050  simpr1l  1056  simp11l  1110  simp21l  1116  simp31l  1122  en2lp  4601  tfisi  4634  funprg  5323  nnsucsssuc  6577  ecopovtrn  6718  ecopovtrng  6721  addassnqg  7494  distrnqg  7499  ltsonq  7510  ltanqg  7512  ltmnqg  7513  distrnq0  7571  addassnq0  7574  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1lem  7892  mulextsr1  7893  axmulass  7985  axdistr  7986  dmdcanap  8794  lt2msq1  8957  ltdiv2  8959  lediv2  8963  xaddass  9990  xaddass2  9991  xlt2add  10001  modqdi  10535  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  resqrtcl  11311  bdtrilem  11521  bdtri  11522  xrbdtri  11558  bitsfzo  12237  prmexpb  12444  4sqlem18  12702  subgabl  13639  opprringbg  13813  cnptoprest  14682  ssblps  14868  ssbl  14869  plyadd  15194  plymul  15195  rplogbchbase  15393  rplogbreexp  15396  relogbcxpbap  15408  lgssq  15488