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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  f1prex  7064  iunfictbso  9627  fin1a2lem13  9925  prlem934  10546  ifle  12686  ixxlb  12856  elfzonelfzo  13243  swrdcl  14109  subcn2  15055  qexpz  16350  mreexexd  17035  initoeu2lem2  17400  issubmnd  18067  gsumccatOLD  18134  frmdup3lem  18160  pmtrf  18714  pgpssslw  18870  lsmmod  18932  reslmhm2b  19958  lsmcl  19987  lbsextlem3  20064  frlmsslsp  20625  islindf4  20667  coe1mul2  21057  coe1fzgsumdlem  21089  evl1gsumdlem  21139  scmate  21274  mdetdiaglem  21362  madurid  21408  cramerlem2  21452  pmatcollpw3lem  21547  iscnp4  22027  cnrest2  22050  ordthauslem  22147  cncmp  22156  clsconn  22194  rnelfmlem  22716  flimrest  22747  isfcf  22798  cnpfcf  22805  alexsubALT  22815  cldsubg  22875  utop2nei  23015  neipcfilu  23061  blssps  23190  blss  23191  stdbdbl  23283  metcnp3  23306  nmoeq0  23502  xrsxmet  23574  metdseq0  23619  addcnlem  23629  xrhmeo  23711  nmhmcn  23885  cfilres  24061  lgsfcl2  26052  lgsdir  26081  lgsne0  26084  istrkgcb  26415  axcontlem2  26924  axcontlem7  26929  axcontlem8  26930  subupgr  27242  clwwlknonex2  28059  frgr3v  28225  pjhthmo  29250  xrge0adddir  30891  dimvalfi  31272  pcmplfinf  31396  probun  31969  satfv1lem  32908  frpomin  33396  fprlem2  33471  nosupbnd1lem3  33569  nosupbnd1lem4  33570  nosupbnd1lem5  33571  nosupbnd2  33575  noinfbnd1lem3  33584  noinfbnd1lem4  33585  noinfbnd1lem5  33586  noinfbnd2  33590  sltlpss  33743  trisegint  33986  btwnconn1lem13  34057  outsideoftr  34087  outsideofeq  34088  linethru  34111  isbasisrelowllem1  35182  atlatmstc  36989  cvlcvr1  37009  hlrelat  37072  intnatN  37077  cvrval5  37085  2at0mat0  37195  llncvrlpln  37228  lplnexllnN  37234  lplncvrlvol  37286  lncvrelatN  37451  lncmp  37453  paddasslem5  37494  pmapjoin  37522  pmapjat1  37523  pclclN  37561  lhprelat3N  37710  cdleme32fvcl  38110  cdlemg1a  38240  cdlemg1cN  38257  cdlemg39  38386  ltrncom  38408  dihmeetALTN  38997  dihlspsnat  39003  mapdrvallem2  39315  sticksstones12  39753  mzpsubst  40183  lzunuz  40203  acongeq  40418  jm2.19  40428  jm2.27  40443  aomclem6  40497  lmhmfgsplit  40524  hbtlem5  40566  iunrelexpuztr  40914  ismnu  41462  3adantll3  42166  ioondisj2  42612  ioondisj1  42613  iccintsng  42642  icccncfext  43011  stoweidlem61  43185  fourierdlem42  43273  fourierdlem73  43303  smflimlem2  43887  domnmsuppn0  45287  lincresunit3  45404  nnolog2flm1  45518  itschlc0xyqsol1  45694  itschlc0xyqsol  45695