Theorem 3simpc 981

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

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

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 965

This theorem is referenced by:  simp3  984  3adant1  1000  3adantl1  1138  3adantr1  1141  eupickb  2084  find  4552  fisseneq  6865  eqsupti  6928  divcanap2  8532  diveqap0  8534  divrecap  8540  divcanap3  8550  eliooord  9810  fzrev3  9967  sqdivap  10461  muldvds2  11686  dvdscmul  11687  dvdsmulc  11688  dvdstr  11697  cncfmptc  12929  cnplimclemr  12985