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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  frpomin  6372  f1prex  7320  poxp3  8191  fprlem2  8342  naddsuc2  8757  iunfictbso  10183  fin1a2lem13  10481  prlem934  11102  ifle  13259  ixxlb  13429  elfzonelfzo  13819  swrdcl  14693  subcn2  15641  qexpz  16948  mreexexd  17706  initoeu2lem2  18082  issubmnd  18799  frmdup3lem  18901  pmtrf  19497  pgpssslw  19656  lsmmod  19717  reslmhm2b  21076  lsmcl  21105  lbsextlem3  21185  frlmsslsp  21839  islindf4  21881  coe1mul2  22293  coe1fzgsumdlem  22328  evl1gsumdlem  22381  scmate  22537  mdetdiaglem  22625  madurid  22671  cramerlem2  22715  pmatcollpw3lem  22810  iscnp4  23292  cnrest2  23315  ordthauslem  23412  cncmp  23421  clsconn  23459  rnelfmlem  23981  flimrest  24012  isfcf  24063  cnpfcf  24070  alexsubALT  24080  cldsubg  24140  utop2nei  24280  neipcfilu  24326  blssps  24455  blss  24456  stdbdbl  24551  metcnp3  24574  nmoeq0  24778  xrsxmet  24850  metdseq0  24895  addcnlem  24905  xrhmeo  24996  nmhmcn  25172  cfilres  25349  lgsfcl2  27365  lgsdir  27394  lgsne0  27397  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd2  27779  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd2  27794  sltlpss  27963  sleadd1  28040  sltmul2  28215  istrkgcb  28482  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  subupgr  29322  clwwlknonex2  30141  frgr3v  30307  pjhthmo  31334  xrge0adddir  33004  dimvalfi  33614  pcmplfinf  33807  probun  34384  satfv1lem  35330  trisegint  35992  btwnconn1lem13  36063  outsideoftr  36093  outsideofeq  36094  linethru  36117  isbasisrelowllem1  37321  atlatmstc  39275  cvlcvr1  39295  hlrelat  39359  intnatN  39364  cvrval5  39372  2at0mat0  39482  llncvrlpln  39515  lplnexllnN  39521  lplncvrlvol  39573  lncvrelatN  39738  lncmp  39740  paddasslem5  39781  pmapjoin  39809  pmapjat1  39810  pclclN  39848  lhprelat3N  39997  cdleme32fvcl  40397  cdlemg1a  40527  cdlemg1cN  40544  cdlemg39  40673  ltrncom  40695  dihmeetALTN  41284  dihlspsnat  41290  mapdrvallem2  41602  sticksstones12  42115  mzpsubst  42704  lzunuz  42724  acongeq  42940  jm2.19  42950  jm2.27  42965  aomclem6  43016  lmhmfgsplit  43043  hbtlem5  43085  nadd2rabtr  43346  iunrelexpuztr  43681  ismnu  44230  3adantll3  44942  ioondisj2  45411  ioondisj1  45412  iccintsng  45441  icccncfext  45808  stoweidlem61  45982  fourierdlem42  46070  fourierdlem73  46100  smflimlem2  46693  domnmsuppn0  48094  lincresunit3  48210  nnolog2flm1  48324  itschlc0xyqsol1  48500  itschlc0xyqsol  48501