Theorem simp1l 1010

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	3ad2ant1 1007	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  simpl1l  1037  simpr1l  1043  simp11l  1097  simp21l  1103  simp31l  1109  en2lp  4525  tfisi  4558  funprg  5232  nnsucsssuc  6451  ecopovtrn  6589  ecopovtrng  6592  addassnqg  7314  distrnqg  7319  ltsonq  7330  ltanqg  7332  ltmnqg  7333  distrnq0  7391  addassnq0  7394  mulasssrg  7690  distrsrg  7691  lttrsr  7694  ltsosr  7696  ltasrg  7702  mulextsr1lem  7712  mulextsr1  7713  axmulass  7805  axdistr  7806  dmdcanap  8609  lt2msq1  8771  ltdiv2  8773  lediv2  8777  xaddass  9796  xaddass2  9797  xlt2add  9807  modqdi  10317  expaddzaplem  10488  expaddzap  10489  expmulzap  10491  resqrtcl  10957  bdtrilem  11166  bdtri  11167  xrbdtri  11203  prmexpb  12060  cnptoprest  12780  ssblps  12966  ssbl  12967  rplogbchbase  13409  rplogbreexp  13412  relogbcxpbap  13424