Theorem simpll1 1209

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 1133	. 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  ordiso2  8963  hartogslem1  8990  wemappo  8997  wemapso2lem  9000  acndom  9462  fin1a2lem12  9822  fin1a2lem13  9823  prlem934  10444  ifle  12578  lcmfunsnlem2lem1  15972  divgcdcoprm0  15999  rpexp  16054  qexpz  16227  ramval  16334  0ram  16346  ramz2  16350  initoeu2lem2  17267  mrelatglb  17786  dfgrp3lem  18189  odbezout  18677  lsmcl  19848  lbsextlem3  19925  frlmsslsp  20485  islindf4  20527  psropprmul  20867  coe1mul2  20898  coe1fzgsumdlem  20930  evl1gsumdlem  20980  scmate  21115  mdetunilem7  21223  mdetmul  21228  cramerlem2  21293  m2pmfzgsumcl  21353  decpmatmul  21377  pmatcollpw3lem  21388  chpdmatlem2  21444  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  chcoeffeqlem  21490  cnconst2  21888  ordthauslem  21988  clsconn  22035  restnlly  22087  comppfsc  22137  ptpjopn  22217  trfg  22496  rnelfmlem  22557  isfcf  22639  fcfnei  22640  cnpfcf  22646  utop2nei  22856  neipcfilu  22902  blssps  23031  blss  23032  metcnp  23148  xrsxmet  23414  metdsge  23454  metdseq0  23459  addcnlem  23469  xrhmeo  23551  nmhmcn  23725  caucfil  23887  limcfval  24475  fta1b  24770  lgsmod  25907  lgsdir  25916  lgsne0  25919  axpasch  26735  axcontlem2  26759  clwwlknonex2  27894  frgr3v  28060  pjhthmo  29085  difioo  30531  xrge0adddir  30726  archiabl  30877  rhmdvdsr  30942  ssmxidl  31050  dimvalfi  31090  probun  31787  satfv1lem  32722  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd2  33329  scutun12  33384  trisegint  33602  btwnconn1lem13  33673  brsegle2  33683  linethru  33727  lindsadd  35050  hlrelat  36698  intnatN  36703  lnnat  36723  3dim0  36753  3dim1  36763  3dim2  36764  atcvrlln  36816  llnexatN  36817  2at0mat0  36821  llncvrlpln  36854  lplnexllnN  36860  lplncvrlvol  36912  lncvrelatN  37077  lncmp  37079  elpaddn0  37096  paddasslem5  37120  pmapjoin  37148  pmapjat1  37149  pclclN  37187  osumclN  37263  lhprelat3N  37336  trlval4  37484  cdlemd5  37498  cdleme32fvcl  37736  cdleme42keg  37782  cdlemg1a  37866  cdlemg1cN  37883  cdlemg39  38012  ltrncom  38034  cdlemk34  38206  dihord2pre  38521  dihopelvalcpre  38544  dihmeetALTN  38623  dihlspsnssN  38628  dihlspsnat  38629  diophrw  39700  lzunuz  39709  qirropth  39849  jm2.19  39934  jm2.27  39949  lmhmfgsplit  40030  hbtlem5  40072  iunrelexpuztr  40420  rfcnnnub  41665  3adantll2  41672  3adantll3  41673  ioondisj2  42130  ioondisj1  42131  iccintsng  42160  icccncfext  42529  stoweidlem20  42662  stoweidlem61  42703  smflimlem2  43405  rmsupp0  44770  rmsuppss  44772  ply1mulgsum  44798  rrxlinesc  45149