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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 1063 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
21adantr 481 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  f1prex  6499  wemappo  8406  iunfictbso  8889  fin1a2lem13  9186  prlem934  9807  ifle  11979  ixxlb  12147  elfzonelfzo  12519  swrdcl  13365  subcn2  14267  qexpz  15540  mreexexd  16240  mreexexdOLD  16241  initoeu2lem2  16597  issubmnd  17250  gsumccat  17310  frmdup3lem  17335  pmtrf  17807  pgpssslw  17961  lsmmod  18020  reslmhm2b  18986  lsmcl  19015  lbsextlem3  19092  coe1mul2  19571  coe1fzgsumdlem  19603  evl1gsumdlem  19652  frlmsslsp  20067  islindf4  20109  scmate  20248  mdetdiaglem  20336  madurid  20382  cramerlem2  20426  pmatcollpw3lem  20520  iscnp4  20990  cnrest2  21013  ordthauslem  21110  cncmp  21118  clsconn  21156  rnelfmlem  21679  flimrest  21710  isfcf  21761  cnpfcf  21768  alexsubALT  21778  cldsubg  21837  utop2nei  21977  neipcfilu  22023  blssps  22152  blss  22153  stdbdbl  22245  metcnp3  22268  nmoeq0  22463  xrsxmet  22535  metdseq0  22580  addcnlem  22590  xrhmeo  22668  nmhmcn  22843  cfilres  23017  lgsfcl2  24945  lgsdir  24974  lgsne0  24977  istrkgcb  25272  axcontlem2  25762  axcontlem7  25767  axcontlem8  25768  subupgr  26089  wpthswwlks2on  26739  frgr3v  27020  pjhthmo  28031  xrge0adddir  29501  pcmplfinf  29734  probun  30286  trisegint  31812  btwnconn1lem13  31883  outsideoftr  31913  outsideofeq  31914  linethru  31937  isbasisrelowllem1  32870  atlatmstc  34121  cvlcvr1  34141  hlrelat  34203  intnatN  34208  cvrval5  34216  2at0mat0  34326  llncvrlpln  34359  lplnexllnN  34365  lplncvrlvol  34417  lncvrelatN  34582  lncmp  34584  paddasslem5  34625  pmapjoin  34653  pmapjat1  34654  pclclN  34692  lhprelat3N  34841  cdleme32fvcl  35243  cdlemg1a  35373  cdlemg1cN  35390  cdlemg39  35519  ltrncom  35541  dihmeetALTN  36131  dihlspsnat  36137  mapdrvallem2  36449  mzpsubst  36826  lzunuz  36846  acongeq  37065  jm2.19  37075  jm2.27  37090  aomclem6  37144  lmhmfgsplit  37171  hbtlem5  37214  iunrelexpuztr  37527  3adantll3  38721  ioondisj2  39156  ioondisj1  39157  iccintsng  39191  icccncfext  39431  stoweidlem61  39611  fourierdlem42  39699  fourierdlem73  39729  smflimlem2  40313  domnmsuppn0  41464  lincresunit3  41584  nnolog2flm1  41702
  Copyright terms: Public domain W3C validator