Theorem 3simpc 1027

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

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

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 1011

This theorem is referenced by:  simp3  1030  3adant1  1046  3adantl1  1184  3adantr1  1187  eupickb  2168  find  4741  fovcld  6183  fisseneq  7232  eqsupti  7326  divcanap2  9000  diveqap0  9002  divrecap  9008  divcanap3  9018  eliooord  10309  fzrev3  10472  sqdivap  11018  swrdlend  11408  swrdnd  11409  ccats1pfxeqbi  11492  muldvds2  12562  dvdscmul  12563  dvdsmulc  12564  dvdstr  12573  rng1zr  14234  srg1zr  14265  domneq0  14554  znleval2  14961  cncfmptc  15620  cnplimclemr  15693  uhgr2edg  16361  umgr2edgneu  16367  clwwlknp  16572