Theorem simp1l 1016

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	3ad2ant1 1013	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simpl1l  1043  simpr1l  1049  simp11l  1103  simp21l  1109  simp31l  1115  en2lp  4538  tfisi  4571  funprg  5248  nnsucsssuc  6471  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  distrnq0  7421  addassnq0  7424  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  dmdcanap  8639  lt2msq1  8801  ltdiv2  8803  lediv2  8807  xaddass  9826  xaddass2  9827  xlt2add  9837  modqdi  10348  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  resqrtcl  10993  bdtrilem  11202  bdtri  11203  xrbdtri  11239  prmexpb  12105  cnptoprest  13033  ssblps  13219  ssbl  13220  rplogbchbase  13662  rplogbreexp  13665  relogbcxpbap  13677  lgssq  13735