Theorem simpll1 1231

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7315  poxp3  8194  naddsuc2  8739  ordiso2  9536  hartogslem1  9563  wemapso2lem  9573  acndom  10157  fin1a2lem12  10516  fin1a2lem13  10517  prlem934  11145  ifle  13354  lcmfunsnlem2lem1  16842  divgcdcoprm0  16869  rpexp  16927  qexpz  17108  ramval  17215  0ram  17227  ramz2  17231  initoeu2lem2  18219  mrelatglb  18763  dfgrp3lem  19277  odbezout  19802  rhmdvdsr  20788  lsmcl  21388  lbsextlem3  21468  rnglidlmcl  21525  frlmsslsp  22132  islindf4  22174  psropprmul  22585  coe1mul2  22618  coe1fzgsumdlem  22651  evl1gsumdlem  22704  scmate  22855  mdetunilem7  22963  mdetmul  22968  cramerlem2  23036  m2pmfzgsumcl  23096  decpmatmul  23120  pmatcollpw3lem  23131  chpdmatlem2  23187  cpmadugsumlemB  23222  cpmadugsumlemC  23223  cpmadugsumlemF  23224  chcoeffeqlem  23233  cnconst2  23631  ordthauslem  23731  clsconn  23778  restnlly  23831  comppfsc  23881  ptpjopn  23961  trfg  24240  rnelfmlem  24301  isfcf  24383  fcfnei  24384  cnpfcf  24390  utop2nei  24599  neipcfilu  24644  blssps  24773  blss  24774  metcnp  24890  xrsxmet  25159  metdsge  25199  metdseq0  25204  addcnlem  25214  xrhmeo  25297  nmhmcn  25471  caucfil  25634  limcfval  26222  fta1b  26520  lgsmod  27680  lgsdir  27689  lgsne0  27692  nosupbnd1lem3  28097  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd2  28103  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  noinfbnd2  28118  cutsun12  28206  ltslpss  28324  leadds1  28405  axpasch  29549  axcontlem2  29573  clwwlknonex2  30730  frgr3v  30906  pjhthmo  31934  difioo  33444  xrge0adddir  33649  archiabl  33829  ssmxidl  34069  dimvalfi  34304  probun  35121  satfv1lem  36294  trisegint  36971  btwnconn1lem13  37042  brsegle2  37052  linethru  37096  lindsadd  38728  hlrelat  40651  intnatN  40656  lnnat  40676  3dim0  40706  3dim1  40716  3dim2  40717  atcvrlln  40769  llnexatN  40770  2at0mat0  40774  llncvrlpln  40807  lplnexllnN  40813  lplncvrlvol  40865  lncvrelatN  41030  lncmp  41032  elpaddn0  41049  paddasslem5  41073  pmapjoin  41101  pmapjat1  41102  pclclN  41140  osumclN  41216  lhprelat3N  41289  trlval4  41437  cdlemd5  41451  cdleme32fvcl  41689  cdleme42keg  41735  cdlemg1a  41819  cdlemg1cN  41836  cdlemg39  41965  ltrncom  41987  cdlemk34  42159  dihord2pre  42474  dihopelvalcpre  42497  dihmeetALTN  42576  dihlspsnssN  42581  dihlspsnat  42582  aks6d1c6isolem1  43416  diophrw  43963  lzunuz  43972  qirropth  44108  jm2.19  44193  jm2.27  44208  lmhmfgsplit  44281  hbtlem5  44322  nadd2rabtr  44578  fzunt  44648  iunrelexpuztr  44911  rfcnnnub  46258  3adantll2  46263  3adantll3  46264  ioondisj2  46710  ioondisj1  46711  iccintsng  46740  icccncfext  47102  stoweidlem20  47235  stoweidlem61  47276  smflimlem2  47987  isuspgrim0lem  49196  isuspgrim0  49197  rmsupp0  49685  rmsuppss  49687  ply1mulgsum  49707  rrxlinesc  50053