Theorem simp1l 967

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  simpl1l  994  simpr1l  1000  simp11l  1054  simp21l  1060  simp31l  1066  en2lp  4370  tfisi  4402  funprg  5064  nnsucsssuc  6253  ecopovtrn  6387  ecopovtrng  6390  addassnqg  6939  distrnqg  6944  ltsonq  6955  ltanqg  6957  ltmnqg  6958  distrnq0  7016  addassnq0  7019  mulasssrg  7302  distrsrg  7303  lttrsr  7306  ltsosr  7308  ltasrg  7314  mulextsr1lem  7323  mulextsr1  7324  axmulass  7406  axdistr  7407  dmdcanap  8187  lt2msq1  8344  ltdiv2  8346  lediv2  8350  modqdi  9795  expaddzaplem  9994  expaddzap  9995  expmulzap  9997  resqrtcl  10458  prmexpb  11404