Theorem simpll1 1035

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

Assertion

Ref	Expression
simpll1

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 999	. 2
2	1	adantr 465	1

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

This theorem is referenced by:  ordiso2  7961  hartogslem1  7988  wemappo  7995  wemapso2lem  7999  acndom  8453  fin1a2lem12  8812  fin1a2lem13  8813  prlem934  9432  ifle  11425  rpexp  14261  qexpz  14420  ramval  14526  0ram  14538  ramz2  14542  mrelatglb  15814  odbezout  16580  lsmcl  17729  lbsextlem3  17806  psropprmul  18279  coe1mul2  18310  coe1fzgsumdlem  18343  evl1gsumdlem  18392  frlmsslsp  18829  frlmsslspOLD  18830  islindf4  18873  scmate  19012  mdetunilem7  19120  mdetmul  19125  cramerlem2  19190  m2pmfzgsumcl  19249  decpmatmul  19273  pmatcollpw3lem  19284  chpdmatlem2  19340  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  chcoeffeqlem  19386  cnconst2  19784  ordthauslem  19884  clscon  19931  restnlly  19983  comppfsc  20033  ptpjopn  20113  trfg  20392  rnelfmlem  20453  isfcf  20535  fcfnei  20536  cnpfcf  20542  utop2nei  20753  neipcfilu  20799  blssps  20927  blss  20928  metcnp  21044  xrsxmet  21314  metdsge  21353  metdseq0  21358  addcnlem  21368  xrhmeo  21446  nmhmcn  21603  caucfil  21722  limcfval  22276  fta1b  22570  lgsmod  23596  lgsdir  23605  lgsne0  23608  axpasch  24244  axcontlem2  24268  clwwlknwwlkncl  24800  clwlkf1clwwlk  24850  pjhthmo  26220  difioo  27593  xrge0adddir  27682  archiabl  27742  rhmdvdsr  27808  probun  28358  trisegint  29678  btwnconn1lem13  29749  brsegle2  29759  linethru  29803  diophrw  30692  lzunuz  30701  qirropth  30844  jm2.19  30935  jm2.27  30950  lmhmfgsplit  31032  hbtlem5  31077  rfcnnnub  31411  3adantll2  31420  3adantll3  31421  ioondisj2  31525  ioondisj1  31526  iccintsng  31563  icccncfext  31690  stoweidlem20  31802  stoweidlem61  31843  initoeu2lem2  32621  rmsupp0  32961  rmsuppss  32963  ply1mulgsum  32990  hlrelat  35126  intnatN  35131  lnnat  35151  3dim0  35181  3dim1  35191  3dim2  35192  atcvrlln  35244  llnexatN  35245  2at0mat0  35249  llncvrlpln  35282  lplnexllnN  35288  lplncvrlvol  35340  lncvrelatN  35505  lncmp  35507  elpaddn0  35524  paddasslem5  35548  pmapjoin  35576  pmapjat1  35577  pclclN  35615  osumclN  35691  lhprelat3N  35764  trlval4  35913  cdlemd5  35927  cdleme32fvcl  36166  cdleme42keg  36212  cdlemg1a  36296  cdlemg1cN  36313  cdlemg39  36442  ltrncom  36464  cdlemk34  36636  dihord2pre  36952  dihopelvalcpre  36975  dihmeetALTN  37054  dihlspsnssN  37059  dihlspsnat  37060

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