Theorem simpll2 1061

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll2	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1025	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  fidceq  7039  fidifsnen  7040  en2eqpr  7080  iunfidisj  7124  ctssdc  7291  cauappcvgprlemlol  7845  caucvgprlemlol  7868  caucvgprprlemlol  7896  elfzonelfzo  10448  qbtwnre  10488  nn0ltexp2  10943  hashun  11039  swrdclg  11197  xrmaxltsup  11784  subcn2  11837  prodmodclem2  12103  divalglemex  12448  divalglemeuneg  12449  dvdslegcd  12500  lcmledvds  12607  modprmn0modprm0  12794  qexpz  12890  rnglidlmcl  14459  iscnp4  14907  cnrest2  14925  blssps  15116  blss  15117  bdbl  15192  metcnp3  15200  addcncntoplem  15250  cdivcncfap  15293  lgsfcl2  15700  lgsdir  15729  lgsne0  15732