MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpll3 Structured version   Visualization version   GIF version

Theorem simpll3 1094
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll3 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 1058 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
21adantr 479 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  f1prex  6417  ordiso2  8281  wemappo  8315  iunfictbso  8798  fin1a2lem12  9094  fin1a2lem13  9095  prlem934  9712  ifle  11864  xlesubadd  11925  icoshftf1o  12125  elfzonelfzo  12394  fsuppmapnn0fiub0  12613  swrdcl  13220  repswccat  13332  subcn2  14122  rpdvds  15161  coprmprod  15162  qexpz  15392  ramval  15499  0ram  15511  cshwrepswhash1  15596  mreexexd  16080  mreexexdOLD  16081  gsumccat  17150  gsmsymgreqlem1  17622  pmtrf  17647  odmulg  17745  pgpfi1  17782  lsmcl  18853  lbsextlem3  18930  coe1mul2  19409  islindf4  19944  cramerlem2  20261  cpmadugsumlemF  20448  cayhamlem4  20460  iscnp4  20825  cnpnei  20826  cnconst2  20845  cnpdis  20855  cnhaus  20916  ordthauslem  20945  clscon  20991  nlly2i  21037  txcn  21187  ordthmeolem  21362  flimrest  21545  isfcf  21596  alexsubALTlem4  21612  ghmcnp  21676  utop2nei  21812  blssps  21987  blss  21988  metcnp3  22103  metcnp  22104  xrsxmet  22368  metdseq0  22413  xrhmeo  22501  cfil3i  22820  caucfil  22834  cfilres  22847  fta1b  23678  mumul  24652  lgsfcl2  24773  lgsdir  24802  lgsne0  24805  istrkgcb  25100  axbtwnid  25565  axcontlem2  25591  axcontlem4  25593  axcontlem7  25596  axcontlem8  25597  pjhthmo  27379  xrge0adddir  28857  archiabl  28917  pcmplfinf  29090  probun  29642  cnpcon  30300  outsideofeq  31241  linethru  31264  atlatmstc  33448  cvlcvr1  33468  ishlat3N  33483  hlrelat  33530  intnatN  33535  cvrval5  33543  atcvrlln  33648  llnexatN  33649  2at0mat0  33653  llncvrlpln  33686  lplnexllnN  33692  lplncvrlvol  33744  lncvrelatN  33909  pmapjoin  33980  pmapjat1  33981  pclclN  34019  osumclN  34095  lhprelat3N  34168  cdlemd5  34331  cdleme32fvcl  34570  cdlemg39  34846  ltrncom  34868  dihmeetALTN  35458  dochss  35496  mapdrvallem2  35776  nacsfix  36117  mzpsubst  36153  diophrw  36164  lzunuz  36173  jm2.19  36402  jm2.27  36417  hbtlem5  36541  iunrelexpuztr  36854  rfcnnnub  38042  3adantll2  38049  infleinf  38353  iccintsng  38420  mullimc  38507  mullimcf  38514  limcperiod  38519  cncfshift  38583  cncfperiod  38588  icccncfext  38597  stoweidlem20  38737  stoweidlem61  38778  fourierdlem73  38896  umgr2v2enb1  40764  wpthswwlks2on  41186  frgr3v  41467  frgr2wwlkeqm  41518  rmsupp0  41965  rmsuppss  41967
  Copyright terms: Public domain W3C validator