Theorem simpll3 1211

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

Step	Hyp	Ref	Expression
1		simp3 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 724	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  f1prex  7298  poxp3  8164  ordiso2  9558  iunfictbso  10157  fin1a2lem12  10454  fin1a2lem13  10455  prlem934  11076  ifle  13230  xlesubadd  13296  icoshftf1o  13505  elfzonelfzo  13789  fsuppmapnn0fiub0  14013  swrdcl  14653  repswccat  14794  subcn2  15597  rpdvds  16661  coprmprod  16662  qexpz  16903  ramval  17010  0ram  17022  cshwrepswhash1  17105  mreexexd  17661  gsmsymgreqlem1  19428  pmtrf  19453  odmulg  19554  pgpfi1  19593  lsmcl  21061  lbsextlem3  21141  islindf4  21836  coe1mul2  22260  cramerlem2  22681  cpmadugsumlemF  22869  cayhamlem4  22881  iscnp4  23258  cnpnei  23259  cnconst2  23278  cnpdis  23288  cnhaus  23349  ordthauslem  23378  clsconn  23425  nlly2i  23471  txcn  23621  ordthmeolem  23796  flimrest  23978  isfcf  24029  alexsubALTlem4  24045  ghmcnp  24110  utop2nei  24246  blssps  24421  blss  24422  metcnp3  24540  metcnp  24541  xrsxmet  24816  metdseq0  24861  xrhmeo  24962  cfil3i  25288  caucfil  25302  cfilres  25315  fta1b  26199  mumul  27209  lgsfcl2  27332  lgsdir  27361  lgsne0  27364  nolt02o  27725  nogt01o  27726  nosupbnd1lem3  27740  nosupbnd1lem4  27741  nosupbnd1lem5  27742  nosupbnd2  27746  noinfbnd1lem3  27755  noinfbnd1lem4  27756  noinfbnd1lem5  27757  noinfbnd2  27761  sleadd1  28003  sltmul2  28172  istrkgcb  28383  axbtwnid  28873  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  umgr2v2enb1  29463  frgr3v  30208  extwwlkfab  30285  pjhthmo  31235  xrge0adddir  32901  archiabl  33063  dimvalfi  33496  pcmplfinf  33676  probun  34253  cnpconn  35058  satfv1lem  35190  outsideofeq  35954  linethru  35977  atlatmstc  39017  cvlcvr1  39037  ishlat3N  39052  hlrelat  39101  intnatN  39106  cvrval5  39114  atcvrlln  39219  llnexatN  39220  2at0mat0  39224  llncvrlpln  39257  lplnexllnN  39263  lplncvrlvol  39315  lncvrelatN  39480  pmapjoin  39551  pmapjat1  39552  pclclN  39590  osumclN  39666  lhprelat3N  39739  cdlemd5  39901  cdleme32fvcl  40139  cdlemg39  40415  ltrncom  40437  dihmeetALTN  41026  dochss  41064  mapdrvallem2  41344  nacsfix  42369  mzpsubst  42405  diophrw  42416  lzunuz  42425  jm2.19  42651  jm2.27  42666  hbtlem5  42789  tfsconcatrn  43008  nadd2rabtr  43050  naddsuc2  43059  fzunt  43122  iunrelexpuztr  43386  grumnudlem  43959  rfcnnnub  44635  3adantll2  44640  infleinf  44987  iccintsng  45141  mullimc  45237  mullimcf  45244  limcperiod  45249  cncfshift  45495  cncfperiod  45500  icccncfext  45508  stoweidlem20  45641  stoweidlem61  45682  fourierdlem73  45800  rmsupp0  47747  rmsuppss  47749  itschlc0xyqsol1  48154  itschlc0xyqsol  48155

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »