Theorem simpll2 1213

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 724	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  frpomin  6338  f1prex  7278  poxp3  8132  fprlem2  8282  iunfictbso  10105  fin1a2lem13  10403  prlem934  11024  ifle  13172  ixxlb  13342  elfzonelfzo  13730  swrdcl  14591  subcn2  15535  qexpz  16830  mreexexd  17588  initoeu2lem2  17961  issubmnd  18648  frmdup3lem  18743  pmtrf  19317  pgpssslw  19476  lsmmod  19537  reslmhm2b  20657  lsmcl  20686  lbsextlem3  20765  frlmsslsp  21342  islindf4  21384  coe1mul2  21782  coe1fzgsumdlem  21816  evl1gsumdlem  21866  scmate  22003  mdetdiaglem  22091  madurid  22137  cramerlem2  22181  pmatcollpw3lem  22276  iscnp4  22758  cnrest2  22781  ordthauslem  22878  cncmp  22887  clsconn  22925  rnelfmlem  23447  flimrest  23478  isfcf  23529  cnpfcf  23536  alexsubALT  23546  cldsubg  23606  utop2nei  23746  neipcfilu  23792  blssps  23921  blss  23922  stdbdbl  24017  metcnp3  24040  nmoeq0  24244  xrsxmet  24316  metdseq0  24361  addcnlem  24371  xrhmeo  24453  nmhmcn  24627  cfilres  24804  lgsfcl2  26795  lgsdir  26824  lgsne0  26827  nosupbnd1lem3  27202  nosupbnd1lem4  27203  nosupbnd1lem5  27204  nosupbnd2  27208  noinfbnd1lem3  27217  noinfbnd1lem4  27218  noinfbnd1lem5  27219  noinfbnd2  27223  sltlpss  27390  sleadd1  27461  sltmul2  27612  istrkgcb  27696  axcontlem2  28212  axcontlem7  28217  axcontlem8  28218  subupgr  28533  clwwlknonex2  29351  frgr3v  29517  pjhthmo  30542  xrge0adddir  32180  dimvalfi  32675  pcmplfinf  32829  probun  33406  satfv1lem  34341  trisegint  34988  btwnconn1lem13  35059  outsideoftr  35089  outsideofeq  35090  linethru  35113  isbasisrelowllem1  36224  atlatmstc  38177  cvlcvr1  38197  hlrelat  38261  intnatN  38266  cvrval5  38274  2at0mat0  38384  llncvrlpln  38417  lplnexllnN  38423  lplncvrlvol  38475  lncvrelatN  38640  lncmp  38642  paddasslem5  38683  pmapjoin  38711  pmapjat1  38712  pclclN  38750  lhprelat3N  38899  cdleme32fvcl  39299  cdlemg1a  39429  cdlemg1cN  39446  cdlemg39  39575  ltrncom  39597  dihmeetALTN  40186  dihlspsnat  40192  mapdrvallem2  40504  sticksstones12  40962  mzpsubst  41471  lzunuz  41491  acongeq  41707  jm2.19  41717  jm2.27  41732  aomclem6  41786  lmhmfgsplit  41813  hbtlem5  41855  nadd2rabtr  42119  naddsuc2  42128  iunrelexpuztr  42455  ismnu  43005  3adantll3  43711  ioondisj2  44192  ioondisj1  44193  iccintsng  44222  icccncfext  44589  stoweidlem61  44763  fourierdlem42  44851  fourierdlem73  44881  smflimlem2  45474  domnmsuppn0  46998  lincresunit3  47115  nnolog2flm1  47229  itschlc0xyqsol1  47405  itschlc0xyqsol  47406