Theorem 3simpc 996

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

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

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 983	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 994	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 121	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

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

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 980

This theorem is referenced by:  simp3  999  3adant1  1015  3adantl1  1153  3adantr1  1156  eupickb  2107  find  4600  fisseneq  6933  eqsupti  6997  divcanap2  8639  diveqap0  8641  divrecap  8647  divcanap3  8657  eliooord  9930  fzrev3  10089  sqdivap  10586  muldvds2  11826  dvdscmul  11827  dvdsmulc  11828  dvdstr  11837  cncfmptc  14167  cnplimclemr  14223