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  7177  fidifsnen  7178  en2eqpr  7220  iunfidisj  7266  fdcf1  7321  ctssdc  7459  cauappcvgprlemlol  8020  caucvgprlemlol  8043  caucvgprprlemlol  8071  elfzonelfzo  10664  qbtwnre  10707  nn0ltexp2  11168  hashun  11266  swrdclg  11443  xrmaxltsup  12048  subcn2  12101  prodmodclem2  12368  divalglemex  12713  divalglemeuneg  12714  dvdslegcd  12765  lcmledvds  12872  modprmn0modprm0  13063  qexpz  13159  rnglidlmcl  14925  iscnp4  15461  cnrest2  15479  blssps  15670  blss  15671  bdbl  15746  metcnp3  15754  addcncntoplem  15804  cdivcncfap  15847  lgsfcl2  16347  lgsdir  16376  lgsne0  16379  subupgr  16736  clwwlknonex2  16902