Theorem simpll2 1064

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 1028	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 1007

This theorem is referenced by:  fidceq  7137  fidifsnen  7138  en2eqpr  7180  iunfidisj  7226  ctssdc  7417  cauappcvgprlemlol  7978  caucvgprlemlol  8001  caucvgprprlemlol  8029  elfzonelfzo  10597  qbtwnre  10640  nn0ltexp2  11096  hashun  11194  swrdclg  11367  xrmaxltsup  11968  subcn2  12021  prodmodclem2  12288  divalglemex  12633  divalglemeuneg  12634  dvdslegcd  12685  lcmledvds  12792  modprmn0modprm0  12979  qexpz  13075  rnglidlmcl  14754  iscnp4  15209  cnrest2  15227  blssps  15418  blss  15419  bdbl  15494  metcnp3  15502  addcncntoplem  15552  cdivcncfap  15595  lgsfcl2  16005  lgsdir  16034  lgsne0  16037  subupgr  16394  clwwlknonex2  16560