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  4620  tfisi  4653  funprg  5343  nnsucsssuc  6601  ecopovtrn  6742  ecopovtrng  6745  addassnqg  7530  distrnqg  7535  ltsonq  7546  ltanqg  7548  ltmnqg  7549  distrnq0  7607  addassnq0  7610  mulasssrg  7906  distrsrg  7907  lttrsr  7910  ltsosr  7912  ltasrg  7918  mulextsr1lem  7928  mulextsr1  7929  axmulass  8021  axdistr  8022  dmdcanap  8830  lt2msq1  8993  ltdiv2  8995  lediv2  8999  xaddass  10026  xaddass2  10027  xlt2add  10037  modqdi  10574  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  swrdspsleq  11158  pfxeq  11187  ccatopth2  11208  pfxccat3  11225  resqrtcl  11455  bdtrilem  11665  bdtri  11666  xrbdtri  11702  bitsfzo  12381  prmexpb  12588  4sqlem18  12846  subgabl  13783  opprringbg  13957  cnptoprest  14826  ssblps  15012  ssbl  15013  plyadd  15338  plymul  15339  rplogbchbase  15537  rplogbreexp  15540  relogbcxpbap  15552  lgssq  15632