Theorem simpll3 1037

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll3

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1001	. 2
2	1	adantr 465	1

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

This theorem is referenced by:  ordiso2  7961  wemappo  7995  iunfictbso  8516  fin1a2lem12  8812  fin1a2lem13  8813  prlem934  9432  ifle  11425  xlesubadd  11484  icoshftf1o  11672  elfzonelfzo  11912  fsuppmapnn0fiub0  12099  swrdcl  12646  repswccat  12757  subcn2  13417  rpdvds  14265  qexpz  14420  ramval  14526  0ram  14538  cshwrepswhash1  14587  mreexexd  15045  gsumccat  16009  gsmsymgreqlem1  16455  pmtrf  16480  odmulg  16578  pgpfi1  16615  lsmcl  17729  lbsextlem3  17806  coe1mul2  18310  islindf4  18873  cramerlem2  19190  cpmadugsumlemF  19377  cayhamlem4  19389  iscnp4  19764  cnpnei  19765  cnconst2  19784  cnpdis  19794  cnhaus  19855  ordthauslem  19884  clscon  19931  nlly2i  19977  txcn  20127  ordthmeolem  20302  flimrest  20484  isfcf  20535  alexsubALTlem4  20550  ghmcnp  20613  utop2nei  20753  blssps  20927  blss  20928  metcnp3  21043  metcnp  21044  xrsxmet  21314  metdseq0  21358  xrhmeo  21446  cfil3i  21708  caucfil  21722  cfilres  21735  fta1b  22570  mumul  23455  lgsfcl2  23577  lgsdir  23605  lgsne0  23608  istrkgcb  23853  axbtwnid  24242  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  pjhthmo  26220  xrge0adddir  27682  archiabl  27742  pcmplfinf  27864  probun  28358  cnpcon  28675  outsideofeq  29780  linethru  29803  nacsfix  30644  mzpsubst  30681  diophrw  30692  lzunuz  30701  jm2.19  30935  jm2.27  30950  hbtlem5  31077  rfcnnnub  31411  3adantll2  31420  iccintsng  31563  mullimc  31622  mullimcf  31629  limcperiod  31634  cncfshift  31676  cncfperiod  31681  icccncfext  31690  stoweidlem20  31802  stoweidlem61  31843  fourierdlem73  31962  rmsupp0  32961  rmsuppss  32963  atlatmstc  35044  cvlcvr1  35064  ishlat3N  35079  hlrelat  35126  intnatN  35131  cvrval5  35139  atcvrlln  35244  llnexatN  35245  2at0mat0  35249  llncvrlpln  35282  lplnexllnN  35288  lplncvrlvol  35340  lncvrelatN  35505  pmapjoin  35576  pmapjat1  35577  pclclN  35615  osumclN  35691  lhprelat3N  35764  cdlemd5  35927  cdleme32fvcl  36166  cdlemg39  36442  ltrncom  36464  dihmeetALTN  37054  dochss  37092  mapdrvallem2  37372

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