Theorem simp1l 970

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

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

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

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

This theorem is referenced by:  simpl1l  997  simpr1l  1003  simp11l  1057  simp21l  1063  simp31l  1069  en2lp  4398  tfisi  4430  funprg  5098  nnsucsssuc  6293  ecopovtrn  6429  ecopovtrng  6432  addassnqg  7038  distrnqg  7043  ltsonq  7054  ltanqg  7056  ltmnqg  7057  distrnq0  7115  addassnq0  7118  mulasssrg  7401  distrsrg  7402  lttrsr  7405  ltsosr  7407  ltasrg  7413  mulextsr1lem  7422  mulextsr1  7423  axmulass  7505  axdistr  7506  dmdcanap  8286  lt2msq1  8443  ltdiv2  8445  lediv2  8449  xaddass  9435  xaddass2  9436  xlt2add  9446  modqdi  9948  expaddzaplem  10129  expaddzap  10130  expmulzap  10132  resqrtcl  10593  bdtrilem  10801  bdtri  10802  xrbdtri  10835  prmexpb  11572  cnptoprest  12105  ssblps  12226  ssbl  12227