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  4645  tfisi  4678  funprg  5370  nnsucsssuc  6636  ecopovtrn  6777  ecopovtrng  6780  addassnqg  7565  distrnqg  7570  ltsonq  7581  ltanqg  7583  ltmnqg  7584  distrnq0  7642  addassnq0  7645  mulasssrg  7941  distrsrg  7942  lttrsr  7945  ltsosr  7947  ltasrg  7953  mulextsr1lem  7963  mulextsr1  7964  axmulass  8056  axdistr  8057  dmdcanap  8865  lt2msq1  9028  ltdiv2  9030  lediv2  9034  xaddass  10061  xaddass2  10062  xlt2add  10072  modqdi  10609  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  swrdspsleq  11194  pfxeq  11223  ccatopth2  11244  pfxccat3  11261  resqrtcl  11535  bdtrilem  11745  bdtri  11746  xrbdtri  11782  bitsfzo  12461  prmexpb  12668  4sqlem18  12926  subgabl  13864  opprringbg  14038  cnptoprest  14907  ssblps  15093  ssbl  15094  plyadd  15419  plymul  15420  rplogbchbase  15618  rplogbreexp  15621  relogbcxpbap  15633  lgssq  15713  uhgr2edg  15998