Theorem simp1l 962

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl1l  989  simpr1l  995  simp11l  1049  simp21l  1055  simp31l  1061  en2lp  4297  tfisi  4328  funprg  4969  nnsucsssuc  6094  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  distrnqg  6577  ltsonq  6588  ltanqg  6590  ltmnqg  6591  distrnq0  6649  addassnq0  6652  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  dmdcanap  7810  lt2msq1  7963  ltdiv2  7965  lediv2  7969  modqdi  9394  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  resqrtcl  9915  prmexpb  10530