Theorem simp1l 1021

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

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

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 980

This theorem is referenced by:  simpl1l  1048  simpr1l  1054  simp11l  1108  simp21l  1114  simp31l  1120  en2lp  4547  tfisi  4580  funprg  5258  nnsucsssuc  6483  ecopovtrn  6622  ecopovtrng  6625  addassnqg  7356  distrnqg  7361  ltsonq  7372  ltanqg  7374  ltmnqg  7375  distrnq0  7433  addassnq0  7436  mulasssrg  7732  distrsrg  7733  lttrsr  7736  ltsosr  7738  ltasrg  7744  mulextsr1lem  7754  mulextsr1  7755  axmulass  7847  axdistr  7848  dmdcanap  8651  lt2msq1  8813  ltdiv2  8815  lediv2  8819  xaddass  9838  xaddass2  9839  xlt2add  9849  modqdi  10360  expaddzaplem  10531  expaddzap  10532  expmulzap  10534  resqrtcl  11004  bdtrilem  11213  bdtri  11214  xrbdtri  11250  prmexpb  12116  cnptoprest  13290  ssblps  13476  ssbl  13477  rplogbchbase  13919  rplogbreexp  13922  relogbcxpbap  13934  lgssq  13992