Theorem simpll3 1040

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll3	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1004	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

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

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  frirrg  4381  fidceq  6925  fidifsnen  6926  en2eqpr  6963  iunfidisj  7005  ordiso2  7094  addlocpr  7596  aptiprlemu  7700  xltadd1  9942  xlesubadd  9949  icoshftf1o  10057  fztri3or  10105  elfzonelfzo  10297  exp3val  10612  nn0ltexp2  10780  hashun  10876  subcn2  11454  divalglemeuneg  12064  dvdslegcd  12101  lcmledvds  12208  rpdvds  12237  cncongr2  12242  qexpz  12490  iuncld  14283  iscnp4  14386  cnpnei  14387  cnconst2  14401  cnpdis  14410  txcn  14443  blssps  14595  blss  14596  metcnp3  14679  metcnp  14680  lgsfcl2  15122  lgsdir  15151  lgsne0  15154