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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 1085 . 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  wemappo  8495  iunfictbso  8975  fin1a2lem13  9272  prlem934  9893  ifle  12066  ixxlb  12235  elfzonelfzo  12610  swrdcl  13464  subcn2  14369  qexpz  15652  mreexexd  16355  mreexexdOLD  16356  initoeu2lem2  16712  issubmnd  17365  gsumccat  17425  frmdup3lem  17450  pmtrf  17921  pgpssslw  18075  lsmmod  18134  reslmhm2b  19102  lsmcl  19131  lbsextlem3  19208  coe1mul2  19687  coe1fzgsumdlem  19719  evl1gsumdlem  19768  frlmsslsp  20183  islindf4  20225  scmate  20364  mdetdiaglem  20452  madurid  20498  cramerlem2  20542  pmatcollpw3lem  20636  iscnp4  21115  cnrest2  21138  ordthauslem  21235  cncmp  21243  clsconn  21281  rnelfmlem  21803  flimrest  21834  isfcf  21885  cnpfcf  21892  alexsubALT  21902  cldsubg  21961  utop2nei  22101  neipcfilu  22147  blssps  22276  blss  22277  stdbdbl  22369  metcnp3  22392  nmoeq0  22587  xrsxmet  22659  metdseq0  22704  addcnlem  22714  xrhmeo  22792  nmhmcn  22966  cfilres  23140  lgsfcl2  25073  lgsdir  25102  lgsne0  25105  istrkgcb  25400  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  subupgr  26224  wpthswwlks2onOLD  26928  clwwlknonex2  27084  frgr3v  27255  pjhthmo  28289  xrge0adddir  29820  pcmplfinf  30056  probun  30609  frpomin  31863  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd2  31987  trisegint  32260  btwnconn1lem13  32331  outsideoftr  32361  outsideofeq  32362  linethru  32385  isbasisrelowllem1  33333  atlatmstc  34924  cvlcvr1  34944  hlrelat  35006  intnatN  35011  cvrval5  35019  2at0mat0  35129  llncvrlpln  35162  lplnexllnN  35168  lplncvrlvol  35220  lncvrelatN  35385  lncmp  35387  paddasslem5  35428  pmapjoin  35456  pmapjat1  35457  pclclN  35495  lhprelat3N  35644  cdleme32fvcl  36045  cdlemg1a  36175  cdlemg1cN  36192  cdlemg39  36321  ltrncom  36343  dihmeetALTN  36933  dihlspsnat  36939  mapdrvallem2  37251  mzpsubst  37628  lzunuz  37648  acongeq  37867  jm2.19  37877  jm2.27  37892  aomclem6  37946  lmhmfgsplit  37973  hbtlem5  38015  iunrelexpuztr  38328  3adantll3  39517  ioondisj2  40032  ioondisj1  40033  iccintsng  40067  icccncfext  40418  stoweidlem61  40596  fourierdlem42  40684  fourierdlem73  40714  smflimlem2  41301  domnmsuppn0  42475  lincresunit3  42595  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator