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  4650  tfisi  4683  funprg  5377  nnsucsssuc  6655  ecopovtrn  6796  ecopovtrng  6799  addassnqg  7592  distrnqg  7597  ltsonq  7608  ltanqg  7610  ltmnqg  7611  distrnq0  7669  addassnq0  7672  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1lem  7990  mulextsr1  7991  axmulass  8083  axdistr  8084  dmdcanap  8892  lt2msq1  9055  ltdiv2  9057  lediv2  9061  xaddass  10094  xaddass2  10095  xlt2add  10105  modqdi  10644  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  swrdspsleq  11238  pfxeq  11267  ccatopth2  11288  pfxccat3  11305  resqrtcl  11580  bdtrilem  11790  bdtri  11791  xrbdtri  11827  bitsfzo  12506  prmexpb  12713  4sqlem18  12971  subgabl  13909  opprringbg  14083  cnptoprest  14953  ssblps  15139  ssbl  15140  plyadd  15465  plymul  15466  rplogbchbase  15664  rplogbreexp  15667  relogbcxpbap  15679  lgssq  15759  uhgr2edg  16045  clwwlkccat  16196