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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 1086 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
21adantr 480 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  f1prex  6579  ordiso2  8461  wemappo  8495  iunfictbso  8975  fin1a2lem12  9271  fin1a2lem13  9272  prlem934  9893  ifle  12066  xlesubadd  12131  icoshftf1o  12333  elfzonelfzo  12610  fsuppmapnn0fiub0  12833  swrdcl  13464  repswccat  13578  subcn2  14369  rpdvds  15421  coprmprod  15422  qexpz  15652  ramval  15759  0ram  15771  cshwrepswhash1  15856  mreexexd  16355  mreexexdOLD  16356  gsumccat  17425  gsmsymgreqlem1  17896  pmtrf  17921  odmulg  18019  pgpfi1  18056  lsmcl  19131  lbsextlem3  19208  coe1mul2  19687  islindf4  20225  cramerlem2  20542  cpmadugsumlemF  20729  cayhamlem4  20741  iscnp4  21115  cnpnei  21116  cnconst2  21135  cnpdis  21145  cnhaus  21206  ordthauslem  21235  clsconn  21281  nlly2i  21327  txcn  21477  ordthmeolem  21652  flimrest  21834  isfcf  21885  alexsubALTlem4  21901  ghmcnp  21965  utop2nei  22101  blssps  22276  blss  22277  metcnp3  22392  metcnp  22393  xrsxmet  22659  metdseq0  22704  xrhmeo  22792  cfil3i  23113  caucfil  23127  cfilres  23140  fta1b  23974  mumul  24952  lgsfcl2  25073  lgsdir  25102  lgsne0  25105  istrkgcb  25400  axbtwnid  25864  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  umgr2v2enb1  26478  wpthswwlks2onOLD  26928  frgr3v  27255  extwwlkfab  27342  pjhthmo  28289  xrge0adddir  29820  archiabl  29880  pcmplfinf  30056  probun  30609  cnpconn  31338  nolt02o  31970  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd2  31987  outsideofeq  32362  linethru  32385  atlatmstc  34924  cvlcvr1  34944  ishlat3N  34959  hlrelat  35006  intnatN  35011  cvrval5  35019  atcvrlln  35124  llnexatN  35125  2at0mat0  35129  llncvrlpln  35162  lplnexllnN  35168  lplncvrlvol  35220  lncvrelatN  35385  pmapjoin  35456  pmapjat1  35457  pclclN  35495  osumclN  35571  lhprelat3N  35644  cdlemd5  35807  cdleme32fvcl  36045  cdlemg39  36321  ltrncom  36343  dihmeetALTN  36933  dochss  36971  mapdrvallem2  37251  nacsfix  37592  mzpsubst  37628  diophrw  37639  lzunuz  37648  jm2.19  37877  jm2.27  37892  hbtlem5  38015  iunrelexpuztr  38328  rfcnnnub  39509  3adantll2  39516  infleinf  39901  iccintsng  40067  mullimc  40166  mullimcf  40173  limcperiod  40178  cncfshift  40405  cncfperiod  40410  icccncfext  40418  stoweidlem20  40555  stoweidlem61  40596  fourierdlem73  40714  rmsupp0  42474  rmsuppss  42476
  Copyright terms: Public domain W3C validator