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  4571  tfisi  4604  funprg  5285  nnsucsssuc  6516  ecopovtrn  6657  ecopovtrng  6660  addassnqg  7410  distrnqg  7415  ltsonq  7426  ltanqg  7428  ltmnqg  7429  distrnq0  7487  addassnq0  7490  mulasssrg  7786  distrsrg  7787  lttrsr  7790  ltsosr  7792  ltasrg  7798  mulextsr1lem  7808  mulextsr1  7809  axmulass  7901  axdistr  7902  dmdcanap  8708  lt2msq1  8871  ltdiv2  8873  lediv2  8877  xaddass  9898  xaddass2  9899  xlt2add  9909  modqdi  10422  expaddzaplem  10593  expaddzap  10594  expmulzap  10596  resqrtcl  11069  bdtrilem  11278  bdtri  11279  xrbdtri  11315  prmexpb  12182  4sqlem18  12439  subgabl  13266  opprringbg  13427  cnptoprest  14191  ssblps  14377  ssbl  14378  rplogbchbase  14820  rplogbreexp  14823  relogbcxpbap  14835  lgssq  14894