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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simp3 1132 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antrr 722 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  f1prex  7034  ordiso2  8968  wemappo  9002  iunfictbso  9529  fin1a2lem12  9822  fin1a2lem13  9823  prlem934  10444  ifle  12580  xlesubadd  12646  icoshftf1o  12850  elfzonelfzo  13129  fsuppmapnn0fiub0  13351  swrdcl  13997  repswccat  14138  subcn2  14941  rpdvds  15994  coprmprod  15995  qexpz  16227  ramval  16334  0ram  16346  cshwrepswhash1  16426  mreexexd  16909  gsumccatOLD  17988  gsmsymgreqlem1  18478  pmtrf  18503  odmulg  18603  pgpfi1  18640  lsmcl  19775  lbsextlem3  19852  coe1mul2  20354  islindf4  20898  cramerlem2  21213  cpmadugsumlemF  21400  cayhamlem4  21412  iscnp4  21787  cnpnei  21788  cnconst2  21807  cnpdis  21817  cnhaus  21878  ordthauslem  21907  clsconn  21954  nlly2i  22000  txcn  22150  ordthmeolem  22325  flimrest  22507  isfcf  22558  alexsubALTlem4  22574  ghmcnp  22638  utop2nei  22774  blssps  22949  blss  22950  metcnp3  23065  metcnp  23066  xrsxmet  23332  metdseq0  23377  xrhmeo  23465  cfil3i  23787  caucfil  23801  cfilres  23814  fta1b  24678  mumul  25672  lgsfcl2  25793  lgsdir  25822  lgsne0  25825  istrkgcb  26156  axbtwnid  26639  axcontlem2  26665  axcontlem4  26667  axcontlem7  26670  axcontlem8  26671  umgr2v2enb1  27222  frgr3v  27968  extwwlkfab  28045  pjhthmo  28993  xrge0adddir  30593  archiabl  30741  dimvalfi  30888  pcmplfinf  31011  probun  31563  cnpconn  32361  satfv1lem  32493  nolt02o  33083  nosupbnd1lem3  33094  nosupbnd1lem4  33095  nosupbnd1lem5  33096  nosupbnd2  33100  outsideofeq  33475  linethru  33498  atlatmstc  36322  cvlcvr1  36342  ishlat3N  36357  hlrelat  36405  intnatN  36410  cvrval5  36418  atcvrlln  36523  llnexatN  36524  2at0mat0  36528  llncvrlpln  36561  lplnexllnN  36567  lplncvrlvol  36619  lncvrelatN  36784  pmapjoin  36855  pmapjat1  36856  pclclN  36894  osumclN  36970  lhprelat3N  37043  cdlemd5  37205  cdleme32fvcl  37443  cdlemg39  37719  ltrncom  37741  dihmeetALTN  38330  dochss  38368  mapdrvallem2  38648  nacsfix  39174  mzpsubst  39210  diophrw  39221  lzunuz  39230  jm2.19  39455  jm2.27  39470  hbtlem5  39593  iunrelexpuztr  39929  grumnudlem  40486  rfcnnnub  41158  3adantll2  41165  infleinf  41505  iccintsng  41664  mullimc  41762  mullimcf  41769  limcperiod  41774  cncfshift  42022  cncfperiod  42027  icccncfext  42035  stoweidlem20  42171  stoweidlem61  42212  fourierdlem73  42330  rmsupp0  44248  rmsuppss  44250  itschlc0xyqsol1  44585  itschlc0xyqsol  44586
  Copyright terms: Public domain W3C validator