Theorem 3simpc 995

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
3simpc

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 978	. 2
2		3simpa 993	. 2
3	1, 2	sylbi 195	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  simp3  998  3adant1  1014  3adantl1  1152  3adantr1  1155  find  6725  tz7.49c  7130  eqsup  7936  mulcanenq  9359  elnpi  9387  divcan2  10240  diveq0  10242  divrec  10248  divcan3  10256  eliooord  11613  fzrev3  11774  modaddabs  12034  modaddmod  12035  modmulmod  12052  sqdiv  12233  swrdlend  12656  ccats1swrdeqbi  12723  sqrmo  13085  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  dvdstr  14018  domneq0  17946  aspid  17979  znleval2  18594  redvr  18653  scmatscmiddistr  19010  1marepvmarrepid  19077  mat2pmatghm  19231  pmatcollpw1lem1  19275  monmatcollpw  19280  pmatcollpwscmatlem2  19291  concompss  19934  islly2  19985  elmptrab2  20329  lmmcvg  21700  ivthicc  21870  aaliou3lem7  22745  logimcl  22957  qrngdiv  23809  ax5seg  24241  usgra2edg1  24383  constr2trl  24601  constr3trllem2  24651  constr3pthlem2  24656  clwwlkfo  24797  clwwlknwwlkncl  24800  clwwisshclww  24807  clwlkfclwwlk  24844  rusgranumwlkg  24958  numclwwlkovgelim  25089  numclwwlk3  25109  ajfuni  25775  funadj  26805  fovcld  27478  trleile  27654  isinftm  27725  cgr3permute1  29698  cgr3com  29703  brifs2  29728  idinside  29734  btwnconn1  29751  lineunray  29797  wl-nfeqfb  29990  pm13.194  31319  fmulcl  31575  fmuldfeqlem1  31576  stoweidlem17  31799  stoweidlem31  31813  sigaraf  32070  sigarmf  32071  pr1eqbg  32297  elfzelfzlble  32337  spthdifv  32352  usgra2pth  32354  usg2edgneu  32412  funcestrcsetclem9  32654  funcsetcestrclem9  32669  funcringcsetcOLD2lem9  32852  funcringcsetclem9OLD  32875  zlmodzxzscm  32946  bnj1098  33842  bnj546  33954  bnj998  34014  bnj1006  34017  bnj1173  34058  bnj1189  34065  riotasv2s  34689  lsatlspsn2  34717  3dim2  35192  paddasslem14  35557  4atexlemex6  35798  cdlemg10bALTN  36362  cdlemg44  36459  tendoplcl  36507  hdmap14lem14  37611

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

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