Theorem 3simpc 874

Description: Simplification of triple conjunction. (The proof was 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 863	. 2 |- ((ph /\ ps /\ ch) <-> (ps /\ ch /\ ph))
2		3simpa 872	. 2 |- ((ps /\ ch /\ ph) -> (ps /\ ch))
3	1, 2	sylbi 216	1 |- ((ph /\ ps /\ ch) -> (ps /\ ch))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  simp3 878  3adant1 894  eupickb 1836  find 3977  tz7.49c 5169  nnleltp1 7138  eliooord 7556  fzrev3 7692  seqzval 7783  ajfuni 9861  psasym 9994  pstr 9995  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pigt2lt4 10024  funadj 11450  bnj636 12571  bnj1169 12961  bnj1192 12969  bnj545 13271  bnj546 13272  bnj998 13363  bnj1004 13369  modaddabs 13612  muldvds2 13679  dvdscmul 13680  dvdsmulc 13681  dvdstr 13687  eqfnung2 14459  cbicplem 14508  cur1val 14546  grpdivzer 14740  elioooord 14855  ismonb2 15161  cmpmon 15164  isepib2 15171  ist1-3 15543  haustlmu 15906  pm13.194 16376  stbval 16731  paddasslem14 17294

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain