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  7027  fidifsnen  7028  en2eqpr  7065  iunfidisj  7109  ctssdc  7276  cauappcvgprlemlol  7830  caucvgprlemlol  7853  caucvgprprlemlol  7881  elfzonelfzo  10431  qbtwnre  10471  nn0ltexp2  10926  hashun  11022  swrdclg  11177  xrmaxltsup  11764  subcn2  11817  prodmodclem2  12083  divalglemex  12428  divalglemeuneg  12429  dvdslegcd  12480  lcmledvds  12587  modprmn0modprm0  12774  qexpz  12870  rnglidlmcl  14438  iscnp4  14886  cnrest2  14904  blssps  15095  blss  15096  bdbl  15171  metcnp3  15179  addcncntoplem  15229  cdivcncfap  15272  lgsfcl2  15679  lgsdir  15708  lgsne0  15711