Theorem simpll1 1093

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 1057	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	adantr 480	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1prex  6439  ordiso2  8303  hartogslem1  8330  wemappo  8337  wemapso2lem  8340  acndom  8757  fin1a2lem12  9116  fin1a2lem13  9117  prlem934  9734  ifle  11902  lcmfunsnlem2lem1  15189  divgcdcoprm0  15217  rpexp  15270  qexpz  15443  ramval  15550  0ram  15562  ramz2  15566  initoeu2lem2  16488  mrelatglb  17007  dfgrp3lem  17336  odbezout  17798  lsmcl  18904  lbsextlem3  18981  psropprmul  19429  coe1mul2  19460  coe1fzgsumdlem  19492  evl1gsumdlem  19541  frlmsslsp  19954  islindf4  19996  scmate  20135  mdetunilem7  20243  mdetmul  20248  cramerlem2  20313  m2pmfzgsumcl  20372  decpmatmul  20396  pmatcollpw3lem  20407  chpdmatlem2  20463  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  chcoeffeqlem  20509  cnconst2  20897  ordthauslem  20997  clscon  21043  restnlly  21095  comppfsc  21145  ptpjopn  21225  trfg  21505  rnelfmlem  21566  isfcf  21648  fcfnei  21649  cnpfcf  21655  utop2nei  21864  neipcfilu  21910  blssps  22039  blss  22040  metcnp  22156  xrsxmet  22420  metdsge  22460  metdseq0  22465  addcnlem  22475  xrhmeo  22553  nmhmcn  22728  caucfil  22889  limcfval  23442  fta1b  23733  lgsmod  24848  lgsdir  24857  lgsne0  24860  axpasch  25621  axcontlem2  25645  clwwlknwwlkncl  26328  clwlkf1clwwlk  26377  pjhthmo  27545  difioo  28934  xrge0adddir  29023  archiabl  29083  rhmdvdsr  29149  probun  29808  trisegint  31305  btwnconn1lem13  31376  brsegle2  31386  linethru  31430  hlrelat  33706  intnatN  33711  lnnat  33731  3dim0  33761  3dim1  33771  3dim2  33772  atcvrlln  33824  llnexatN  33825  2at0mat0  33829  llncvrlpln  33862  lplnexllnN  33868  lplncvrlvol  33920  lncvrelatN  34085  lncmp  34087  elpaddn0  34104  paddasslem5  34128  pmapjoin  34156  pmapjat1  34157  pclclN  34195  osumclN  34271  lhprelat3N  34344  trlval4  34493  cdlemd5  34507  cdleme32fvcl  34746  cdleme42keg  34792  cdlemg1a  34876  cdlemg1cN  34893  cdlemg39  35022  ltrncom  35044  cdlemk34  35216  dihord2pre  35532  dihopelvalcpre  35555  dihmeetALTN  35634  dihlspsnssN  35639  dihlspsnat  35640  diophrw  36340  lzunuz  36349  qirropth  36491  jm2.19  36578  jm2.27  36593  lmhmfgsplit  36674  hbtlem5  36717  iunrelexpuztr  37030  rfcnnnub  38218  3adantll2  38225  3adantll3  38226  ioondisj2  38561  ioondisj1  38562  iccintsng  38596  icccncfext  38773  stoweidlem20  38913  stoweidlem61  38954  smflimlem2  39658  wpthswwlks2on  41164  clwwlksnwwlkncl  41228  frgr3v  41445  frgr2wwlkeqm  41496  rmsupp0  41943  rmsuppss  41945  ply1mulgsum  41972