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  4591  tfisi  4624  funprg  5309  nnsucsssuc  6559  ecopovtrn  6700  ecopovtrng  6703  addassnqg  7466  distrnqg  7471  ltsonq  7482  ltanqg  7484  ltmnqg  7485  distrnq0  7543  addassnq0  7546  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  dmdcanap  8766  lt2msq1  8929  ltdiv2  8931  lediv2  8935  xaddass  9961  xaddass2  9962  xlt2add  9972  modqdi  10501  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  resqrtcl  11211  bdtrilem  11421  bdtri  11422  xrbdtri  11458  bitsfzo  12137  prmexpb  12344  4sqlem18  12602  subgabl  13538  opprringbg  13712  cnptoprest  14559  ssblps  14745  ssbl  14746  plyadd  15071  plymul  15072  rplogbchbase  15270  rplogbreexp  15273  relogbcxpbap  15285  lgssq  15365