Theorem simpll 730

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
simpll	|- (((ph /\ ps) /\ ch) -> ph)

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (ph -> ph)
2	1	ad2antrr 706	1 |- (((ph /\ ps) /\ ch) -> ph)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  simp1ll  1018  simp2ll  1022  simp3ll  1026  pm2.61da3ne  2597  rmob  3135  ifboth  3694  nndisjeq  4430  preaddccan2  4456  ltfinirr  4458  lenltfin  4470  sfintfin  4533  tfinnn  4535  imainss  5043  ncdisjun  6137  sbth  6207  leconnnc  6219  tlecg  6231  lemuc1  6254  nchoicelem4  6293  nchoicelem19  6308  nchoice  6309