Theorem simpll1 1212

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 1136	. 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:  f1prex  7320  poxp3  8191  naddsuc2  8757  ordiso2  9584  hartogslem1  9611  wemapso2lem  9621  acndom  10120  fin1a2lem12  10480  fin1a2lem13  10481  prlem934  11102  ifle  13259  lcmfunsnlem2lem1  16685  divgcdcoprm0  16712  rpexp  16769  qexpz  16948  ramval  17055  0ram  17067  ramz2  17071  initoeu2lem2  18082  mrelatglb  18630  dfgrp3lem  19078  odbezout  19600  rhmdvdsr  20534  lsmcl  21105  lbsextlem3  21185  rnglidlmcl  21249  frlmsslsp  21839  islindf4  21881  psropprmul  22260  coe1mul2  22293  coe1fzgsumdlem  22328  evl1gsumdlem  22381  scmate  22537  mdetunilem7  22645  mdetmul  22650  cramerlem2  22715  m2pmfzgsumcl  22775  decpmatmul  22799  pmatcollpw3lem  22810  chpdmatlem2  22866  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  chcoeffeqlem  22912  cnconst2  23312  ordthauslem  23412  clsconn  23459  restnlly  23511  comppfsc  23561  ptpjopn  23641  trfg  23920  rnelfmlem  23981  isfcf  24063  fcfnei  24064  cnpfcf  24070  utop2nei  24280  neipcfilu  24326  blssps  24455  blss  24456  metcnp  24575  xrsxmet  24850  metdsge  24890  metdseq0  24895  addcnlem  24905  xrhmeo  24996  nmhmcn  25172  caucfil  25336  limcfval  25927  fta1b  26231  lgsmod  27385  lgsdir  27394  lgsne0  27397  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd2  27779  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd2  27794  scutun12  27873  sltlpss  27963  sleadd1  28040  axpasch  28974  axcontlem2  28998  clwwlknonex2  30141  frgr3v  30307  pjhthmo  31334  difioo  32787  xrge0adddir  33004  archiabl  33178  ssmxidl  33467  dimvalfi  33614  probun  34384  satfv1lem  35330  trisegint  35992  btwnconn1lem13  36063  brsegle2  36073  linethru  36117  lindsadd  37573  hlrelat  39359  intnatN  39364  lnnat  39384  3dim0  39414  3dim1  39424  3dim2  39425  atcvrlln  39477  llnexatN  39478  2at0mat0  39482  llncvrlpln  39515  lplnexllnN  39521  lplncvrlvol  39573  lncvrelatN  39738  lncmp  39740  elpaddn0  39757  paddasslem5  39781  pmapjoin  39809  pmapjat1  39810  pclclN  39848  osumclN  39924  lhprelat3N  39997  trlval4  40145  cdlemd5  40159  cdleme32fvcl  40397  cdleme42keg  40443  cdlemg1a  40527  cdlemg1cN  40544  cdlemg39  40673  ltrncom  40695  cdlemk34  40867  dihord2pre  41182  dihopelvalcpre  41205  dihmeetALTN  41284  dihlspsnssN  41289  dihlspsnat  41290  aks6d1c6isolem1  42131  diophrw  42715  lzunuz  42724  qirropth  42864  jm2.19  42950  jm2.27  42965  lmhmfgsplit  43043  hbtlem5  43085  nadd2rabtr  43346  fzunt  43417  iunrelexpuztr  43681  rfcnnnub  44936  3adantll2  44941  3adantll3  44942  ioondisj2  45411  ioondisj1  45412  iccintsng  45441  icccncfext  45808  stoweidlem20  45941  stoweidlem61  45982  smflimlem2  46693  isuspgrim0lem  47755  isuspgrim0  47756  rmsupp0  48093  rmsuppss  48095  ply1mulgsum  48119  rrxlinesc  48469