Theorem simp1l 1024

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

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

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 983

This theorem is referenced by:  simpl1l  1051  simpr1l  1057  simp11l  1111  simp21l  1117  simp31l  1123  en2lp  4602  tfisi  4635  funprg  5324  nnsucsssuc  6578  ecopovtrn  6719  ecopovtrng  6722  addassnqg  7495  distrnqg  7500  ltsonq  7511  ltanqg  7513  ltmnqg  7514  distrnq0  7572  addassnq0  7575  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1lem  7893  mulextsr1  7894  axmulass  7986  axdistr  7987  dmdcanap  8795  lt2msq1  8958  ltdiv2  8960  lediv2  8964  xaddass  9991  xaddass2  9992  xlt2add  10002  modqdi  10537  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  swrdspsleq  11120  resqrtcl  11340  bdtrilem  11550  bdtri  11551  xrbdtri  11587  bitsfzo  12266  prmexpb  12473  4sqlem18  12731  subgabl  13668  opprringbg  13842  cnptoprest  14711  ssblps  14897  ssbl  14898  plyadd  15223  plymul  15224  rplogbchbase  15422  rplogbreexp  15425  relogbcxpbap  15437  lgssq  15517