Theorem simpll2 1032

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  fidceq  6847  fidifsnen  6848  en2eqpr  6885  iunfidisj  6923  ctssdc  7090  cauappcvgprlemlol  7609  caucvgprlemlol  7632  caucvgprprlemlol  7660  elfzonelfzo  10186  qbtwnre  10213  nn0ltexp2  10644  hashun  10740  xrmaxltsup  11221  subcn2  11274  prodmodclem2  11540  divalglemex  11881  divalglemeuneg  11882  dvdslegcd  11919  lcmledvds  12024  modprmn0modprm0  12210  qexpz  12304  iscnp4  13012  cnrest2  13030  blssps  13221  blss  13222  bdbl  13297  metcnp3  13305  addcncntoplem  13345  cdivcncfap  13381  lgsfcl2  13701  lgsdir  13730  lgsne0  13733