Theorem simpll2 1036

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

Assertion

Ref	Expression
simpll2

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1000	. 2
2	1	adantr 465	1

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

This theorem is referenced by:  wemappo  7995  iunfictbso  8516  fin1a2lem13  8813  prlem934  9432  ifle  11425  ixxlb  11580  elfzonelfzo  11912  swrdcl  12646  subcn2  13417  qexpz  14420  mreexexd  15045  issubmnd  15948  gsumccat  16009  frmdup3lem  16034  pmtrf  16480  pgpssslw  16634  lsmmod  16693  reslmhm2b  17700  lsmcl  17729  lbsextlem3  17806  coe1mul2  18310  coe1fzgsumdlem  18343  evl1gsumdlem  18392  frlmsslsp  18829  frlmsslspOLD  18830  islindf4  18873  scmate  19012  mdetdiaglem  19100  madurid  19146  cramerlem2  19190  pmatcollpw3lem  19284  iscnp4  19764  cnrest2  19787  ordthauslem  19884  cncmp  19892  clscon  19931  rnelfmlem  20453  flimrest  20484  isfcf  20535  cnpfcf  20542  alexsubALT  20551  cldsubg  20609  utop2nei  20753  neipcfilu  20799  blssps  20927  blss  20928  stdbdbl  21020  metcnp3  21043  nmoeq0  21243  xrsxmet  21314  metdseq0  21358  addcnlem  21368  xrhmeo  21446  nmhmcn  21603  cfilres  21735  lgsfcl2  23577  lgsdir  23605  lgsne0  23608  istrkgcb  23853  axcontlem2  24268  axcontlem7  24273  axcontlem8  24274  usg2spot2nb  25065  pjhthmo  26220  xrge0adddir  27682  pcmplfinf  27864  probun  28358  trisegint  29678  btwnconn1lem13  29749  outsideoftr  29779  outsideofeq  29780  linethru  29803  mzpsubst  30681  lzunuz  30701  acongeq  30921  jm2.19  30935  jm2.27  30950  aomclem6  31005  lmhmfgsplit  31032  hbtlem5  31077  3adantll3  31421  ioondisj2  31525  ioondisj1  31526  iccintsng  31563  icccncfext  31690  stoweidlem61  31843  fourierdlem42  31931  fourierdlem73  31962  initoeu2lem2  32621  domnmsuppn0  32962  lincresunit3  33082  atlatmstc  35044  cvlcvr1  35064  hlrelat  35126  intnatN  35131  cvrval5  35139  2at0mat0  35249  llncvrlpln  35282  lplnexllnN  35288  lplncvrlvol  35340  lncvrelatN  35505  lncmp  35507  paddasslem5  35548  pmapjoin  35576  pmapjat1  35577  pclclN  35615  lhprelat3N  35764  cdleme32fvcl  36166  cdlemg1a  36296  cdlemg1cN  36313  cdlemg39  36442  ltrncom  36464  dihmeetALTN  37054  dihlspsnat  37060  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