Theorem 3simpc 1023

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 1010	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 1021	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 121	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

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

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 1007

This theorem is referenced by:  simp3  1026  3adant1  1042  3adantl1  1180  3adantr1  1183  eupickb  2164  find  4726  fovcld  6166  fisseneq  7208  eqsupti  7300  divcanap2  8971  diveqap0  8973  divrecap  8979  divcanap3  8989  eliooord  10280  fzrev3  10443  sqdivap  10989  swrdlend  11375  swrdnd  11376  ccats1pfxeqbi  11459  muldvds2  12528  dvdscmul  12529  dvdsmulc  12530  dvdstr  12539  rng1zr  14199  srg1zr  14230  domneq0  14519  znleval2  14928  cncfmptc  15587  cnplimclemr  15660  uhgr2edg  16327  umgr2edgneu  16333  clwwlknp  16538