Theorem simpll3 1233

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 1156	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 739	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7321  poxp3  8202  naddsuc2  8747  ordiso2  9544  iunfictbso  10230  fin1a2lem12  10526  fin1a2lem13  10527  prlem934  11155  ifle  13365  xlesubadd  13431  icoshftf1o  13643  elfzonelfzo  13942  fsuppmapnn0fiub0  14174  swrdcl  14833  repswccat  14977  subcn2  15803  rpdvds  16876  coprmprod  16877  qexpz  17120  ramval  17227  0ram  17239  cshwrepswhash1  17321  mreexexd  17863  gsmsymgreqlem1  19686  pmtrf  19711  odmulg  19812  pgpfi1  19851  lsmcl  21400  lbsextlem3  21480  islindf4  22188  coe1mul2  22632  cramerlem2  23050  cpmadugsumlemF  23238  cayhamlem4  23250  iscnp4  23625  cnpnei  23626  cnconst2  23645  cnpdis  23655  cnhaus  23716  ordthauslem  23745  clsconn  23792  nlly2i  23839  txcn  23989  ordthmeolem  24164  flimrest  24346  isfcf  24397  alexsubALTlem4  24413  ghmcnp  24478  utop2nei  24613  blssps  24787  blss  24788  metcnp3  24903  metcnp  24904  xrsxmet  25173  metdseq0  25218  xrhmeo  25311  cfil3i  25634  caucfil  25648  cfilres  25661  fta1b  26534  mumul  27554  lgsfcl2  27676  lgsdir  27705  lgsne0  27708  nolt02o  28098  nogt01o  28099  nosupbnd1lem3  28113  nosupbnd1lem4  28114  nosupbnd1lem5  28115  nosupbnd2  28119  noinfbnd1lem3  28128  noinfbnd1lem4  28129  noinfbnd1lem5  28130  noinfbnd2  28134  leadds1  28421  ltmuls2  28603  istrkgcb  28964  axbtwnid  29563  axcontlem2  29589  axcontlem4  29591  axcontlem7  29594  axcontlem8  29595  umgr2v2enb1  30153  frgr3v  30922  extwwlkfab  30999  pjhthmo  31950  xrge0adddir  33668  archiabl  33848  dimvalfi  34338  pcmplfinf  34597  probun  35155  cnpconn  36196  satfv1lem  36328  outsideofeq  37103  linethru  37126  weiunso  37462  atlatmstc  40635  cvlcvr1  40655  ishlat3N  40670  hlrelat  40718  intnatN  40723  cvrval5  40731  atcvrlln  40836  llnexatN  40837  2at0mat0  40841  llncvrlpln  40874  lplnexllnN  40880  lplncvrlvol  40932  lncvrelatN  41097  pmapjoin  41168  pmapjat1  41169  pclclN  41207  osumclN  41283  lhprelat3N  41356  cdlemd5  41518  cdleme32fvcl  41756  cdlemg39  42032  ltrncom  42054  dihmeetALTN  42643  dochss  42681  mapdrvallem2  42961  nacsfix  43983  mzpsubst  44019  diophrw  44030  lzunuz  44039  jm2.19  44260  jm2.27  44275  hbtlem5  44389  tfsconcatrn  44599  nadd2rabtr  44641  fzunt  44711  iunrelexpuztr  44974  grumnudlem  45524  rfcnnnub  46321  3adantll2  46326  infleinf  46650  iccintsng  46802  mullimc  46895  mullimcf  46902  limcperiod  46907  cncfshift  47151  cncfperiod  47156  icccncfext  47164  stoweidlem20  47297  stoweidlem61  47338  fourierdlem73  47456  rmsupp0  49805  rmsuppss  49807  itschlc0xyqsol1  50203  itschlc0xyqsol  50204