Theorem simpll2 1068

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ctssdc  7453  cauappcvgprlemlol  8014  caucvgprlemlol  8037  caucvgprprlemlol  8065  elfzonelfzo  10658  qbtwnre  10701  nn0ltexp2  11161  hashun  11259  swrdclg  11436  xrmaxltsup  12040  subcn2  12093  prodmodclem2  12360  divalglemex  12705  divalglemeuneg  12706  dvdslegcd  12757  lcmledvds  12864  modprmn0modprm0  13055  qexpz  13151  rnglidlmcl  14866  iscnp4  15368  cnrest2  15386  blssps  15577  blss  15578  bdbl  15653  metcnp3  15661  addcncntoplem  15711  cdivcncfap  15754  lgsfcl2  16223  lgsdir  16252  lgsne0  16255  subupgr  16612  clwwlknonex2  16778