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

Theorem simpll2 1214
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpll2 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpll2
StepHypRef Expression
1 simp2 1138 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antrr 725 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  frpomin  6298  f1prex  7234  poxp3  8086  fprlem2  8236  iunfictbso  10058  fin1a2lem13  10356  prlem934  10977  ifle  13125  ixxlb  13295  elfzonelfzo  13683  swrdcl  14542  subcn2  15486  qexpz  16781  mreexexd  17536  initoeu2lem2  17909  issubmnd  18591  frmdup3lem  18684  pmtrf  19245  pgpssslw  19404  lsmmod  19465  reslmhm2b  20559  lsmcl  20588  lbsextlem3  20666  frlmsslsp  21225  islindf4  21267  coe1mul2  21663  coe1fzgsumdlem  21695  evl1gsumdlem  21745  scmate  21882  mdetdiaglem  21970  madurid  22016  cramerlem2  22060  pmatcollpw3lem  22155  iscnp4  22637  cnrest2  22660  ordthauslem  22757  cncmp  22766  clsconn  22804  rnelfmlem  23326  flimrest  23357  isfcf  23408  cnpfcf  23415  alexsubALT  23425  cldsubg  23485  utop2nei  23625  neipcfilu  23671  blssps  23800  blss  23801  stdbdbl  23896  metcnp3  23919  nmoeq0  24123  xrsxmet  24195  metdseq0  24240  addcnlem  24250  xrhmeo  24332  nmhmcn  24506  cfilres  24683  lgsfcl2  26674  lgsdir  26703  lgsne0  26706  nosupbnd1lem3  27081  nosupbnd1lem4  27082  nosupbnd1lem5  27083  nosupbnd2  27087  noinfbnd1lem3  27096  noinfbnd1lem4  27097  noinfbnd1lem5  27098  noinfbnd2  27102  sltlpss  27265  sleadd1  27327  istrkgcb  27447  axcontlem2  27963  axcontlem7  27968  axcontlem8  27969  subupgr  28284  clwwlknonex2  29102  frgr3v  29268  pjhthmo  30293  xrge0adddir  31939  dimvalfi  32363  pcmplfinf  32506  probun  33083  satfv1lem  34020  trisegint  34666  btwnconn1lem13  34737  outsideoftr  34767  outsideofeq  34768  linethru  34791  isbasisrelowllem1  35876  atlatmstc  37831  cvlcvr1  37851  hlrelat  37915  intnatN  37920  cvrval5  37928  2at0mat0  38038  llncvrlpln  38071  lplnexllnN  38077  lplncvrlvol  38129  lncvrelatN  38294  lncmp  38296  paddasslem5  38337  pmapjoin  38365  pmapjat1  38366  pclclN  38404  lhprelat3N  38553  cdleme32fvcl  38953  cdlemg1a  39083  cdlemg1cN  39100  cdlemg39  39229  ltrncom  39251  dihmeetALTN  39840  dihlspsnat  39846  mapdrvallem2  40158  sticksstones12  40616  mzpsubst  41118  lzunuz  41138  acongeq  41354  jm2.19  41364  jm2.27  41379  aomclem6  41433  lmhmfgsplit  41460  hbtlem5  41502  nadd2rabtr  41747  naddsuc2  41756  iunrelexpuztr  42083  ismnu  42633  3adantll3  43339  ioondisj2  43821  ioondisj1  43822  iccintsng  43851  icccncfext  44218  stoweidlem61  44392  fourierdlem42  44480  fourierdlem73  44510  smflimlem2  45103  domnmsuppn0  46535  lincresunit3  46652  nnolog2flm1  46766  itschlc0xyqsol1  46942  itschlc0xyqsol  46943
  Copyright terms: Public domain W3C validator