Theorem 3simpc 991

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 978	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 989	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 120	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

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  ax-ia3 107

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

This theorem is referenced by:  simp3  994  3adant1  1010  3adantl1  1148  3adantr1  1151  eupickb  2100  find  4583  fisseneq  6909  eqsupti  6973  divcanap2  8597  diveqap0  8599  divrecap  8605  divcanap3  8615  eliooord  9885  fzrev3  10043  sqdivap  10540  muldvds2  11779  dvdscmul  11780  dvdsmulc  11781  dvdstr  11790  cncfmptc  13376  cnplimclemr  13432