Theorem simp1l 1047

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

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

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 1006

This theorem is referenced by:  simpl1l  1074  simpr1l  1080  simp11l  1134  simp21l  1140  simp31l  1146  en2lp  4652  tfisi  4685  funprg  5380  nnsucsssuc  6659  ecopovtrn  6800  ecopovtrng  6803  addassnqg  7601  distrnqg  7606  ltsonq  7617  ltanqg  7619  ltmnqg  7620  distrnq0  7678  addassnq0  7681  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  dmdcanap  8901  lt2msq1  9064  ltdiv2  9066  lediv2  9070  xaddass  10103  xaddass2  10104  xlt2add  10114  modqdi  10653  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  swrdspsleq  11247  pfxeq  11276  ccatopth2  11297  pfxccat3  11314  resqrtcl  11589  bdtrilem  11799  bdtri  11800  xrbdtri  11836  bitsfzo  12515  prmexpb  12722  4sqlem18  12980  subgabl  13918  opprringbg  14092  cnptoprest  14962  ssblps  15148  ssbl  15149  plyadd  15474  plymul  15475  rplogbchbase  15673  rplogbreexp  15676  relogbcxpbap  15688  lgssq  15768  uhgr2edg  16056  clwwlkccat  16251