Theorem simp1l 1045

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

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

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 1004

This theorem is referenced by:  simpl1l  1072  simpr1l  1078  simp11l  1132  simp21l  1138  simp31l  1144  en2lp  4646  tfisi  4679  funprg  5371  nnsucsssuc  6646  ecopovtrn  6787  ecopovtrng  6790  addassnqg  7580  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  distrnq0  7657  addassnq0  7660  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1lem  7978  mulextsr1  7979  axmulass  8071  axdistr  8072  dmdcanap  8880  lt2msq1  9043  ltdiv2  9045  lediv2  9049  xaddass  10077  xaddass2  10078  xlt2add  10088  modqdi  10626  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  swrdspsleq  11214  pfxeq  11243  ccatopth2  11264  pfxccat3  11281  resqrtcl  11555  bdtrilem  11765  bdtri  11766  xrbdtri  11802  bitsfzo  12481  prmexpb  12688  4sqlem18  12946  subgabl  13884  opprringbg  14058  cnptoprest  14928  ssblps  15114  ssbl  15115  plyadd  15440  plymul  15441  rplogbchbase  15639  rplogbreexp  15642  relogbcxpbap  15654  lgssq  15734  uhgr2edg  16019  clwwlkccat  16138