Theorem simpll2 1210

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  f1prex  7018  wemappo  8997  iunfictbso  9525  fin1a2lem13  9823  prlem934  10444  ifle  12578  ixxlb  12748  elfzonelfzo  13134  swrdcl  13998  subcn2  14943  qexpz  16227  mreexexd  16911  initoeu2lem2  17267  issubmnd  17930  gsumccatOLD  17997  frmdup3lem  18023  pmtrf  18575  pgpssslw  18731  lsmmod  18793  reslmhm2b  19819  lsmcl  19848  lbsextlem3  19925  frlmsslsp  20485  islindf4  20527  coe1mul2  20898  coe1fzgsumdlem  20930  evl1gsumdlem  20980  scmate  21115  mdetdiaglem  21203  madurid  21249  cramerlem2  21293  pmatcollpw3lem  21388  iscnp4  21868  cnrest2  21891  ordthauslem  21988  cncmp  21997  clsconn  22035  rnelfmlem  22557  flimrest  22588  isfcf  22639  cnpfcf  22646  alexsubALT  22656  cldsubg  22716  utop2nei  22856  neipcfilu  22902  blssps  23031  blss  23032  stdbdbl  23124  metcnp3  23147  nmoeq0  23342  xrsxmet  23414  metdseq0  23459  addcnlem  23469  xrhmeo  23551  nmhmcn  23725  cfilres  23900  lgsfcl2  25887  lgsdir  25916  lgsne0  25919  istrkgcb  26250  axcontlem2  26759  axcontlem7  26764  axcontlem8  26765  subupgr  27077  clwwlknonex2  27894  frgr3v  28060  pjhthmo  29085  xrge0adddir  30726  dimvalfi  31090  pcmplfinf  31214  probun  31787  satfv1lem  32722  frpomin  33191  fprlem2  33251  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd2  33329  trisegint  33602  btwnconn1lem13  33673  outsideoftr  33703  outsideofeq  33704  linethru  33727  isbasisrelowllem1  34772  atlatmstc  36615  cvlcvr1  36635  hlrelat  36698  intnatN  36703  cvrval5  36711  2at0mat0  36821  llncvrlpln  36854  lplnexllnN  36860  lplncvrlvol  36912  lncvrelatN  37077  lncmp  37079  paddasslem5  37120  pmapjoin  37148  pmapjat1  37149  pclclN  37187  lhprelat3N  37336  cdleme32fvcl  37736  cdlemg1a  37866  cdlemg1cN  37883  cdlemg39  38012  ltrncom  38034  dihmeetALTN  38623  dihlspsnat  38629  mapdrvallem2  38941  mzpsubst  39689  lzunuz  39709  acongeq  39924  jm2.19  39934  jm2.27  39949  aomclem6  40003  lmhmfgsplit  40030  hbtlem5  40072  iunrelexpuztr  40420  ismnu  40969  3adantll3  41673  ioondisj2  42130  ioondisj1  42131  iccintsng  42160  icccncfext  42529  stoweidlem61  42703  fourierdlem42  42791  fourierdlem73  42821  smflimlem2  43405  domnmsuppn0  44771  lincresunit3  44890  nnolog2flm1  45004  itschlc0xyqsol1  45180  itschlc0xyqsol  45181