Theorem simpl1 1057

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1054	. 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:  simpll1  1093  simprl1  1099  simp1l1  1147  simp2l1  1153  simp3l1  1159  3anandirs  1427  rspc3ev  3297  f1prex  6439  cocan1  6446  weniso  6504  smogt  7351  smorndom  7352  omeulem1  7549  nnmord  7599  nnmword  7600  difsnen  7927  enfixsn  7954  mapunen  8014  ac6sfi  8089  fipreima  8155  elfiun  8219  ordiso2  8303  wemaplem2  8335  wemapso  8339  en2eqpr  8713  indcardi  8747  fodomfi2  8766  iunfictbso  8820  infmap2  8923  cofsmo  8974  cfsmolem  8975  coftr  8978  fin23lem11  9022  fincssdom  9028  fin23lem26  9030  isf32lem9  9066  ac6num  9184  gchdomtri  9330  gchpwdom  9371  winainflem  9394  tskuni  9484  gruima  9503  gruf  9512  grudomon  9518  elnpi  9689  distrlem4pr  9727  prlem934  9734  addcan  10099  addcan2  10100  divmulass  10587  divmulasscom  10588  ltmul1a  10751  suprleub  10866  supmul1  10869  suprzcl  11333  uzsupss  11656  xleadd1a  11955  xlesubadd  11965  xmulasslem3  11988  xlemul2a  11991  xadddilem  11996  xadddi2  11999  ixxun  12062  icoshftf1o  12166  snunioc  12171  lincmb01cmp  12186  iccf1o  12187  nn0p1elfzo  12378  fzofzim  12382  ltexp2a  12774  leexp2  12777  ltexp2r  12779  exple1  12782  expnlbnd2  12857  fun2dmnop0  13131  ccatass  13224  ccat2s1fvw  13267  swrdswrdlem  13311  ccatopth  13322  cshimadifsn  13426  cshimadifsn0  13427  cshco  13433  repsco  13436  s2f1o  13511  limsupgre  14060  addcn2  14172  mulcn2  14174  ntrivcvgmul  14473  binomrisefac  14612  dvdsadd2b  14866  dvdsmod  14888  oexpneg  14907  sadass  15031  gcdass  15102  rplpwr  15114  rppwr  15115  lcmfunsnlem1  15188  coprmdvds2  15206  rpmulgcd2  15208  qredeq  15209  rpdvds  15212  cncongr2  15220  rpexp  15270  prmdiveq  15329  hashgcdlem  15331  odzdvds  15338  modprmn0modprm0  15350  coprimeprodsq2  15352  pythagtriplem3  15361  pcdvdsb  15411  pcgcd1  15419  qexpz  15443  pockthg  15448  vdwnnlem1  15537  0ram  15562  ramz2  15566  lubss  16944  lubun  16946  clatleglb  16949  clatglbss  16950  mrelatglb  17007  isnsgrp  17111  issubmnd  17141  ress0g  17142  gsumccat  17201  frmdss2  17223  mulgneg  17383  mulgdirlem  17395  submmulg  17409  subgmulg  17431  nmzsubg  17458  ghmmulg  17495  gsmsymgreqlem1  17673  pmtrfb  17708  psgnunilem4  17740  odmodnn0  17782  odnncl  17787  odmod  17788  odmulgid  17794  odmulgeq  17797  odf1o1  17810  odf1o2  17811  odngen  17815  gexdvdsi  17821  pgpfi1  17833  odcau  17842  subgslw  17854  fislw  17863  lsmssv  17881  lsmless1x  17882  lsmless2x  17883  lsmsubm  17891  lsmmod  17911  lsmmod2  17912  efgred  17984  cntzcmn  18068  ghmplusg  18072  odadd1  18074  odadd2  18075  odadd  18076  lsmcomx  18082  gsumconst  18157  srg1zr  18352  ring1eq0  18413  mulgass2  18424  isabvd  18643  lssintcl  18785  0lmhm  18861  lmhmvsca  18866  reslmhm2b  18875  pwssplit1  18880  pwssplit3  18882  lspfixed  18949  lspsnat  18966  lidldvgen  19076  issubassa  19145  evlsval2  19341  psrplusgpropd  19427  coe1subfv  19457  coe1mul2  19460  xrsdsreclblem  19611  regsumsupp  19787  obselocv  19891  uvcresum  19951  frlmsslsp  19954  frlmup4  19959  lindff1  19978  f1lindf  19980  lsslindf  19988  islindf4  19996  lbslcic  19999  mhmvlin  20022  mpt2matmul  20071  mamutpos  20083  scmatscmide  20132  mavmulsolcl  20176  marrepcl  20189  mdetdiag  20224  mdetunilem1  20237  mdetunilem3  20239  mdetunilem7  20243  mdetunilem9  20245  mdetmul  20248  slesolinvbi  20306  m2pmfzmap  20371  pmatcollpwlem  20404  pmatcollpw  20405  mp2pm2mplem4  20433  chpdmatlem3  20464  chfacfisfcpmat  20479  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmidpmatlem2  20495  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  riinopn  20538  neiint  20718  topssnei  20738  restntr  20796  iscnp4  20877  cnconst2  20897  cnrest2  20900  cnprest2  20904  cnpdis  20907  cnt0  20960  cnt1  20964  cnhaus  20968  ordthauslem  20997  cncmp  21005  fiuncmp  21017  sscmp  21018  hauscmp  21020  cnconn  21035  uncon  21042  nlly2i  21089  llynlly  21090  nllyidm  21102  finlocfin  21133  ptrescn  21252  xkococnlem  21272  qtoptop2  21312  qtopss  21328  kqfvima  21343  r0cld  21351  ordthmeolem  21414  fbssint  21452  fmf  21559  fmss  21560  elfm  21561  rnelfmlem  21566  rnelfm  21567  fmco  21575  flimss2  21586  flimss1  21587  flimrest  21597  flftg  21610  cnpflf2  21614  cnpflf  21615  flfcnp  21618  supnfcls  21634  fclsss1  21636  fclsss2  21637  fcfnei  21649  fcfelbas  21650  cnpfcfi  21654  subgntr  21720  opnsubg  21721  cldsubg  21724  ghmcnp  21728  utop2nei  21864  neipcfilu  21910  bldisj  22013  blgt0  22014  bl2in  22015  blss2ps  22018  blss2  22019  blssps  22039  blss  22040  xmetresbl  22052  lpbl  22118  blcld  22120  stdbdbl  22132  metcnp3  22155  metcnp2  22157  txmetcnp  22162  blval2  22177  nmoix  22343  nmoeq0  22350  icoopnst  22546  iocopnst  22547  xrhmeo  22553  nmhmcn  22728  cphsqrtcl2  22794  cphsqrtcl3  22795  cfil3i  22875  caublcls  22915  bcthlem5  22933  cmetcusp1  22957  rrxcph  22988  pjth  23018  ovoliunlem2  23078  volun  23120  volsup2  23179  mbfimaopn2  23230  iblconst  23390  itgconst  23391  dvcnp2  23489  dvcn  23490  deg1mul3le  23680  deg1tmle  23681  dvdsq1p  23724  ig1peu  23735  ig1pdvds  23740  coeid3  23800  dgrmulc  23831  efcvx  24007  tanord  24088  logdivlti  24170  logccv  24209  recxpcl  24221  cxpeq  24298  ang180  24344  isosctrlem2  24349  cxp2lim  24503  amgm  24517  muval1  24659  dvdssqf  24664  mumullem2  24706  mumul  24707  bcmono  24802  lgsfcl2  24828  lgsdilem  24849  lgsdirprm  24856  lgsdir  24857  lgsdi  24859  lgsne0  24860  padicabv  25119  brbtwn2  25585  colinearalglem1  25586  colinearalg  25590  axcgrtr  25595  axsegconlem8  25604  axsegconlem9  25605  axsegconlem10  25606  axcontlem8  25651  axcontlem10  25653  2pthon  26132  clwwlkfo  26325  clwwlkext2edg  26330  erclwwlksym  26342  erclwwlknsym  26354  clwlkfoclwwlk  26372  clwlkf1clwwlklem  26376  numclwwlk2lem1  26629  numclwwlk5  26639  frgraregord13  26646  nvmul0or  26889  ipval2lem2  26943  lnomul  26999  shless  27602  shlej1  27603  pjspansn  27820  hoadddi  28046  kbmul  28198  homco2  28220  kbass2  28360  eliccelico  28929  elicoelioo  28930  iocinioc2  28931  iocinif  28933  xrge0adddir  29023  xrge0npcan  29025  archiabl  29083  ress1r  29120  rhmdvdsr  29149  pstmfval  29267  fmcncfil  29305  zrhnm  29341  qqhnm  29362  measvunilem  29602  volfiniune  29620  dya2iocnrect  29670  sibfinima  29728  probun  29808  probinc  29810  cndprob01  29824  bnj517  30209  bnj594  30236  pconpi1  30473  cvmsss2  30510  mrsubcv  30661  msubvrs  30711  dvdspw  30889  br6  30900  br4  30901  frrlem4  31027  cgrcomim  31266  cgrtriv  31279  cgrextend  31285  segconeq  31287  btwntriv2  31289  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  trisegint  31305  cgrsub  31322  cgrxfr  31332  btwnxfr  31333  lineext  31353  btwnconn1lem13  31376  btwnconn1lem14  31377  btwnconn3  31380  segcon2  31382  brsegle  31385  brsegle2  31386  segletr  31391  segleantisym  31392  seglelin  31393  outsideofeu  31408  lineunray  31424  lineelsb2  31425  ivthALT  31500  lindsenlbs  32574  areacirc  32675  cocanfo  32682  upixp  32694  ismtyima  32772  rrndstprj2  32800  zerdivemp1x  32916  lsatfixedN  33314  lssat  33321  eqlkr  33404  eqlkr2  33405  lkrlsp  33407  lshpkrlem4  33418  opposet  33486  cvrcon3b  33582  cvrcmp  33588  atlen0  33615  atnle  33622  atlatmstc  33624  cvlatexch3  33643  cvlsupr2  33648  hlsupr2  33691  hlrelat2  33707  cvrexchlem  33723  lnnat  33731  atcvrj2b  33736  atle  33740  atexchcvrN  33744  atbtwn  33750  athgt  33760  3dimlem3  33765  3dim1  33771  1cvratlt  33778  1cvrjat  33779  ps-1  33781  ps-2  33782  3atlem3  33789  3atlem5  33791  3atlem7  33793  llni  33812  llni2  33816  atcvrlln2  33823  llnexatN  33825  llncmp  33826  2llnmat  33828  2at0mat0  33829  lplni  33836  lplnnle2at  33845  2atnelpln  33848  lplnllnneN  33860  llncvrlpln2  33861  2lplnmN  33863  2llnmj  33864  lplncmp  33866  lplnexatN  33867  lplnexllnN  33868  2llnm3N  33873  lvoli  33879  lvoli3  33881  islvol2aN  33896  4atlem0a  33897  4atlem3  33900  4atlem3a  33901  4atlem4a  33903  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  4atlem10b  33909  4atlem11  33913  4atlem12  33916  lplncvrlvol2  33919  lvolcmp  33921  2lplnmj  33926  islinei  34044  pmapglbx  34073  linepmap  34079  lneq2at  34082  lnjatN  34084  lncvrat  34086  lncmp  34087  2llnma3r  34092  elpaddatriN  34107  elpaddat  34108  paddcom  34117  paddss1  34121  paddss2  34122  paddss12  34123  paddasslem6  34129  paddasslem7  34130  paddasslem8  34131  paddasslem9  34132  paddasslem15  34138  pmodlem2  34151  pmodl42N  34155  pmapjoin  34156  llnmod1i2  34164  2polcon4bN  34222  polcon2bN  34224  poml4N  34257  poml6N  34259  osumcllem1N  34260  osumcllem2N  34261  osumcllem11N  34270  osumclN  34271  pmapojoinN  34272  pexmidlem2N  34275  pexmidlem3N  34276  pexmidlem4N  34277  pexmidlem6N  34279  pexmidlem7N  34280  pl42lem2N  34284  pl42lem3N  34285  pl42lem4N  34286  pl42N  34287  lhpexle2lem  34313  lhpexle3lem  34315  lhpexle3  34316  lhpmcvr3  34329  lhp2at0nle  34339  lhprelat3N  34344  4atex  34380  4atex2  34381  lauteq  34399  lautco  34401  ltrncoidN  34432  ltrneq2  34452  ltrnnidn  34479  ltrnideq  34480  trlnid  34484  ltrnatlw  34488  trlnle  34491  trlval3  34492  trlval4  34493  cdlemc  34502  cdlemd5  34507  cdlemd9  34511  ltrneq3  34513  cdleme0moN  34530  cdleme20  34630  cdleme21j  34642  cdleme21  34643  cdleme27cl  34672  cdlemefrs29bpre0  34702  cdlemefs27cl  34719  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme32d  34750  cdleme32f  34752  cdleme32le  34753  cdleme35h2  34763  cdleme38n  34770  cdleme40m  34773  cdleme41snaw  34782  cdleme42ke  34791  cdleme17d3  34802  cdleme48fvg  34806  cdlemeg46fvcl  34812  cdlemeg46fgN  34840  cdleme48gfv1  34842  cdleme48fgv  34844  cdleme50trn3  34859  trlord  34875  ltrniotavalbN  34890  cdlemb3  34912  cdlemg6c  34926  cdlemg6  34929  cdlemg7N  34932  cdlemg8c  34935  cdlemg8  34937  cdlemg11a  34943  cdlemg11b  34948  cdlemg12e  34953  cdlemg15a  34961  cdlemg15  34962  cdlemg16  34963  cdlemg16z  34965  cdlemg16zz  34966  cdlemg17dN  34969  cdlemg18a  34984  cdlemg20  34991  cdlemg22  34993  cdlemg24  34994  cdlemg37  34995  cdlemg31d  35006  cdlemg29  35011  cdlemg33b  35013  cdlemg33  35017  cdlemg38  35021  cdlemg39  35022  cdlemg40  35023  trlco  35033  trlcone  35034  cdlemg42  35035  cdlemg44b  35038  ltrncom  35044  trljco  35046  tendococl  35078  tendoplcl  35087  tendoplcom  35088  cdlemj2  35128  cdlemj3  35129  tendoid0  35131  tendoconid  35135  tendotr  35136  cdlemk25-3  35210  cdlemk26b-3  35211  cdlemk34  35216  cdlemk36  35219  cdlemk38  35221  cdlemkid4  35240  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk19x  35249  cdlemk53  35263  cdlemk55  35267  cdlemk55u  35272  cdlemk39u  35274  cdlemk19u  35276  cdlemk56  35277  tendoex  35281  cdleml3N  35284  cdleml5N  35286  tendospcanN  35330  cdlemm10N  35425  cdlemn11pre  35517  dihord2pre  35532  dihvalcqpre  35542  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihord  35571  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetbN  35610  dihmeetlem4preN  35613  dihmeetlem5  35615  dihmeetlem7N  35617  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem12N  35625  dihmeetlem13N  35626  dihmeetlem15N  35628  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem18N  35631  dihmeetlem19N  35632  dihmeetALTN  35634  dih1dimatlem0  35635  dihlspsnssN  35639  dihlspsnat  35640  mapdh8ad  36086  hdmap14lem14  36191  hgmapvvlem3  36235  mzprename  36330  eldioph2lem1  36341  lzunuz  36349  rencldnfi  36403  pellexlem2  36412  infmrgelbi  36460  pellfundglb  36467  pellfund14gap  36469  qirropth  36491  rmxycomplete  36500  congadd  36551  acongeq  36568  jm2.19  36578  jm2.23  36581  jm2.20nn  36582  jm2.27  36593  jm3.1  36605  aomclem6  36647  lnmepi  36673  lmhmfgsplit  36674  lmhmlnmsplit  36675  pwssplit4  36677  hbtlem2  36713  hbtlem5  36717  dgraa0p  36738  proot1hash  36797  iocunico  36815  relexpxpmin  37028  brtrclfv2  37038  ntrclsiso  37385  ntrclskb  37387  ntrclsk3  37388  k0004lem3  37467  suprnmpt  38350  wessf1ornlem  38366  projf1o  38381  snunioo2  38578  snunioo1  38585  iccintsng  38596  lptre2pt  38707  limcleqr  38711  fnlimfvre  38741  volioc  38864  iblspltprt  38865  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem28  38921  stoweidlem34  38927  stoweidlem44  38937  stoweidlem60  38953  wallispilem3  38960  fourierdlem41  39041  fourierdlem42  39042  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem74  39073  fourierdlem97  39096  caratheodorylem2  39417  ovnsubaddlem2  39461  hspmbllem2  39517  fzopredsuc  39946  iccpartigtl  39961  lighneal  40066  oexpnegALTV  40126  oexpnegnz  40127  tgblthelfgott  40229  tgblthelfgottOLD  40236  repswpfx  40299  fzoopth  40360  vtxdlfuhgr1v  40694  umgr2wlk  41156  clwwlksfo  41225  clwwlksext2edg  41230  erclwwlkssym  41242  erclwwlksnsym  41254  clwlksf1clwwlklem  41275  av-numclwwlk2lem1  41532  av-numclwwlk5  41542  av-frgraregord13  41550  lidldomn1  41711  ofaddmndmap  41915  lincdifsn  42007  lincellss  42009  lincresunit3lem3  42057  islindeps2  42066  lindssnlvec  42069  fdivmptf  42133  refdivmptf  42134