Theorem simpll1 1219

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpll1	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simp1 1142	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 732	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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

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

This theorem is referenced by:  f1prex  7235  poxp3  8097  naddsuc2  8634  ordiso2  9427  hartogslem1  9454  wemapso2lem  9464  acndom  9971  fin1a2lem12  10331  fin1a2lem13  10332  prlem934  10954  ifle  13147  lcmfunsnlem2lem1  16605  divgcdcoprm0  16632  rpexp  16690  qexpz  16870  ramval  16977  0ram  16989  ramz2  16993  initoeu2lem2  17980  mrelatglb  18524  dfgrp3lem  19012  odbezout  19531  rhmdvdsr  20487  lsmcl  21080  lbsextlem3  21160  rnglidlmcl  21216  frlmsslsp  21778  islindf4  21820  psropprmul  22229  coe1mul2  22262  coe1fzgsumdlem  22296  evl1gsumdlem  22349  scmate  22500  mdetunilem7  22608  mdetmul  22613  cramerlem2  22678  m2pmfzgsumcl  22738  decpmatmul  22762  pmatcollpw3lem  22773  chpdmatlem2  22829  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  chcoeffeqlem  22875  cnconst2  23273  ordthauslem  23373  clsconn  23420  restnlly  23472  comppfsc  23522  ptpjopn  23602  trfg  23881  rnelfmlem  23942  isfcf  24024  fcfnei  24025  cnpfcf  24031  utop2nei  24240  neipcfilu  24285  blssps  24414  blss  24415  metcnp  24531  xrsxmet  24800  metdsge  24840  metdseq0  24845  addcnlem  24855  xrhmeo  24938  nmhmcn  25112  caucfil  25275  limcfval  25864  fta1b  26162  lgsmod  27311  lgsdir  27320  lgsne0  27323  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd2  27705  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd2  27720  cutsun12  27807  ltslpss  27925  leadds1  28006  axpasch  29035  axcontlem2  29059  clwwlknonex2  30204  frgr3v  30370  pjhthmo  31398  difioo  32881  xrge0adddir  33104  archiabl  33286  ssmxidl  33564  dimvalfi  33793  probun  34610  satfv1lem  35597  trisegint  36263  btwnconn1lem13  36334  brsegle2  36344  linethru  36388  lindsadd  37987  hlrelat  39901  intnatN  39906  lnnat  39926  3dim0  39956  3dim1  39966  3dim2  39967  atcvrlln  40019  llnexatN  40020  2at0mat0  40024  llncvrlpln  40057  lplnexllnN  40063  lplncvrlvol  40115  lncvrelatN  40280  lncmp  40282  elpaddn0  40299  paddasslem5  40323  pmapjoin  40351  pmapjat1  40352  pclclN  40390  osumclN  40466  lhprelat3N  40539  trlval4  40687  cdlemd5  40701  cdleme32fvcl  40939  cdleme42keg  40985  cdlemg1a  41069  cdlemg1cN  41086  cdlemg39  41215  ltrncom  41237  cdlemk34  41409  dihord2pre  41724  dihopelvalcpre  41747  dihmeetALTN  41826  dihlspsnssN  41831  dihlspsnat  41832  aks6d1c6isolem1  42666  diophrw  43215  lzunuz  43224  qirropth  43360  jm2.19  43445  jm2.27  43460  lmhmfgsplit  43538  hbtlem5  43580  nadd2rabtr  43836  fzunt  43906  iunrelexpuztr  44170  rfcnnnub  45491  3adantll2  45496  3adantll3  45497  ioondisj2  45945  ioondisj1  45946  iccintsng  45975  icccncfext  46337  stoweidlem20  46470  stoweidlem61  46511  smflimlem2  47222  isuspgrim0lem  48391  isuspgrim0  48392  rmsupp0  48866  rmsuppss  48868  ply1mulgsum  48888  rrxlinesc  49233