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

Step	Hyp	Ref	Expression
1		simp2 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrr 726	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  frpomin  6298  f1prex  7230  poxp3  8092  fprlem2  8243  naddsuc2  8629  iunfictbso  10024  fin1a2lem13  10322  prlem934  10944  ifle  13112  ixxlb  13283  elfzonelfzo  13685  swrdcl  14569  subcn2  15518  qexpz  16829  mreexexd  17571  initoeu2lem2  17939  issubmnd  18686  frmdup3lem  18791  pmtrf  19384  pgpssslw  19543  lsmmod  19604  reslmhm2b  21006  lsmcl  21035  lbsextlem3  21115  frlmsslsp  21751  islindf4  21793  coe1mul2  22211  coe1fzgsumdlem  22247  evl1gsumdlem  22300  scmate  22454  mdetdiaglem  22542  madurid  22588  cramerlem2  22632  pmatcollpw3lem  22727  iscnp4  23207  cnrest2  23230  ordthauslem  23327  cncmp  23336  clsconn  23374  rnelfmlem  23896  flimrest  23927  isfcf  23978  cnpfcf  23985  alexsubALT  23995  cldsubg  24055  utop2nei  24194  neipcfilu  24239  blssps  24368  blss  24369  stdbdbl  24461  metcnp3  24484  nmoeq0  24680  xrsxmet  24754  metdseq0  24799  addcnlem  24809  xrhmeo  24900  nmhmcn  25076  cfilres  25252  lgsfcl2  27270  lgsdir  27299  lgsne0  27302  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd2  27684  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd2  27699  ltslpss  27904  leadds1  27985  ltmuls2  28167  bdayfinbndlem1  28463  istrkgcb  28528  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  subupgr  29360  clwwlknonex2  30184  frgr3v  30350  pjhthmo  31377  xrge0adddir  33100  dimvalfi  33758  pcmplfinf  34018  probun  34576  satfv1lem  35556  trisegint  36222  btwnconn1lem13  36293  outsideoftr  36323  outsideofeq  36324  linethru  36347  isbasisrelowllem1  37560  atlatmstc  39579  cvlcvr1  39599  hlrelat  39662  intnatN  39667  cvrval5  39675  2at0mat0  39785  llncvrlpln  39818  lplnexllnN  39824  lplncvrlvol  39876  lncvrelatN  40041  lncmp  40043  paddasslem5  40084  pmapjoin  40112  pmapjat1  40113  pclclN  40151  lhprelat3N  40300  cdleme32fvcl  40700  cdlemg1a  40830  cdlemg1cN  40847  cdlemg39  40976  ltrncom  40998  dihmeetALTN  41587  dihlspsnat  41593  mapdrvallem2  41905  sticksstones12  42412  mzpsubst  42990  lzunuz  43010  acongeq  43225  jm2.19  43235  jm2.27  43250  aomclem6  43301  lmhmfgsplit  43328  hbtlem5  43370  nadd2rabtr  43626  iunrelexpuztr  43960  ismnu  44502  3adantll3  45287  ioondisj2  45739  ioondisj1  45740  iccintsng  45769  icccncfext  46131  stoweidlem61  46305  fourierdlem42  46393  fourierdlem73  46423  smflimlem2  47016  domnmsuppn0  48615  lincresunit3  48727  nnolog2flm1  48836  itschlc0xyqsol1  49012  itschlc0xyqsol  49013