Theorem simpl1 1064

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 481	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpll1  1100  simprl1  1106  simp1l1  1154  simp2l1  1160  simp3l1  1166  3anandirs  1435  rspc3ev  3326  f1prex  6539  cocan1  6546  weniso  6604  smogt  7464  smorndom  7465  omeulem1  7662  nnmord  7712  nnmword  7713  difsnen  8042  enfixsn  8069  mapunen  8129  ac6sfi  8204  fipreima  8272  elfiun  8336  ordiso2  8420  wemaplem2  8452  wemapso  8456  en2eqpr  8830  indcardi  8864  fodomfi2  8883  iunfictbso  8937  infmap2  9040  cofsmo  9091  cfsmolem  9092  coftr  9095  fin23lem11  9139  fincssdom  9145  fin23lem26  9147  isf32lem9  9183  ac6num  9301  gchdomtri  9451  gchpwdom  9492  winainflem  9515  tskuni  9605  gruima  9624  gruf  9633  grudomon  9639  elnpi  9810  distrlem4pr  9848  prlem934  9855  addcan  10220  addcan2  10221  divmulass  10708  divmulasscom  10709  ltmul1a  10872  suprleub  10989  supmul1  10992  suprzcl  11457  uzsupss  11780  xleadd1a  12083  xlesubadd  12093  xmulasslem3  12116  xlemul2a  12119  xadddilem  12124  xadddi2  12127  ixxun  12191  icoshftf1o  12295  snunioc  12300  lincmb01cmp  12315  iccf1o  12316  nn0p1elfzo  12510  fzofzim  12514  ltexp2a  12912  leexp2  12915  ltexp2r  12917  exple1  12920  expnlbnd2  12995  fun2dmnop0  13276  ccatass  13371  ccat2s1fvw  13415  swrdswrdlem  13459  ccatopth  13470  cshimadifsn  13575  cshimadifsn0  13576  cshco  13582  repsco  13585  s2f1o  13661  limsupgre  14212  addcn2  14324  mulcn2  14326  ntrivcvgmul  14634  binomrisefac  14773  dvdsadd2b  15028  dvdsmod  15050  oexpneg  15069  sadass  15193  gcdass  15264  rplpwr  15276  rppwr  15277  lcmfunsnlem1  15350  coprmdvds2  15368  rpmulgcd2  15370  qredeq  15371  rpdvds  15374  cncongr2  15382  rpexp  15432  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  modprmn0modprm0  15512  coprimeprodsq2  15514  pythagtriplem3  15523  pcdvdsb  15573  pcgcd1  15581  qexpz  15605  pockthg  15610  vdwnnlem1  15699  0ram  15724  ramz2  15728  lubss  17121  lubun  17123  clatleglb  17126  clatglbss  17127  mrelatglb  17184  isnsgrp  17288  issubmnd  17318  ress0g  17319  gsumccat  17378  frmdss2  17400  mulgneg  17560  mulgdirlem  17572  submmulg  17586  subgmulg  17608  nmzsubg  17635  ghmmulg  17672  gsmsymgreqlem1  17850  pmtrfb  17885  psgnunilem4  17917  odmodnn0  17959  odnncl  17964  odmod  17965  odmulgid  17971  odmulgeq  17974  odf1o1  17987  odf1o2  17988  odngen  17992  gexdvdsi  17998  pgpfi1  18010  odcau  18019  subgslw  18031  fislw  18040  lsmssv  18058  lsmless1x  18059  lsmless2x  18060  lsmsubm  18068  lsmmod  18088  lsmmod2  18089  efgred  18161  cntzcmn  18245  ghmplusg  18249  odadd1  18251  odadd2  18252  odadd  18253  lsmcomx  18259  gsumconst  18334  srg1zr  18529  ring1eq0  18590  mulgass2  18601  isabvd  18820  rmodislmodlem  18930  rmodislmod  18931  lssintcl  18964  0lmhm  19040  lmhmvsca  19045  reslmhm2b  19054  pwssplit1  19059  pwssplit3  19061  lspfixed  19128  lspsnat  19145  lidldvgen  19255  issubassa  19324  evlsval2  19520  psrplusgpropd  19606  coe1subfv  19636  coe1mul2  19639  xrsdsreclblem  19792  regsumsupp  19968  obselocv  20072  uvcresum  20132  frlmsslsp  20135  frlmup4  20140  lindff1  20159  f1lindf  20161  lsslindf  20169  islindf4  20177  lbslcic  20180  mhmvlin  20203  mpt2matmul  20252  mamutpos  20264  scmatscmide  20313  mavmulsolcl  20357  marrepcl  20370  mdetdiag  20405  mdetunilem1  20418  mdetunilem3  20420  mdetunilem7  20424  mdetunilem9  20426  mdetmul  20429  slesolinvbi  20487  m2pmfzmap  20552  pmatcollpwlem  20585  pmatcollpw  20586  mp2pm2mplem4  20614  chpdmatlem3  20645  chfacfisfcpmat  20660  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmidpmatlem2  20676  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  riinopn  20713  neiint  20908  topssnei  20928  restntr  20986  iscnp4  21067  cnconst2  21087  cnrest2  21090  cnprest2  21094  cnpdis  21097  cnt0  21150  cnt1  21154  cnhaus  21158  ordthauslem  21187  cncmp  21195  fiuncmp  21207  sscmp  21208  hauscmp  21210  cnconn  21225  unconn  21232  nlly2i  21279  llynlly  21280  nllyidm  21292  finlocfin  21323  ptrescn  21442  xkococnlem  21462  qtoptop2  21502  qtopss  21518  kqfvima  21533  r0cld  21541  ordthmeolem  21604  fbssint  21642  fmf  21749  fmss  21750  elfm  21751  rnelfmlem  21756  rnelfm  21757  fmco  21765  flimss2  21776  flimss1  21777  flimrest  21787  flftg  21800  cnpflf2  21804  cnpflf  21805  flfcnp  21808  supnfcls  21824  fclsss1  21826  fclsss2  21827  fcfnei  21839  fcfelbas  21840  cnpfcfi  21844  subgntr  21910  opnsubg  21911  cldsubg  21914  ghmcnp  21918  utop2nei  22054  neipcfilu  22100  bldisj  22203  blgt0  22204  bl2in  22205  blss2ps  22208  blss2  22209  blssps  22229  blss  22230  xmetresbl  22242  lpbl  22308  blcld  22310  stdbdbl  22322  metcnp3  22345  metcnp2  22347  txmetcnp  22352  blval2  22367  nmoix  22533  nmoeq0  22540  icoopnst  22738  iocopnst  22739  xrhmeo  22745  nmhmcn  22920  cphsqrtcl2  22986  cphsqrtcl3  22987  cfil3i  23067  caublcls  23107  bcthlem5  23125  cmetcusp1  23149  rrxcph  23180  pjth  23210  ovoliunlem2  23271  volun  23313  volsup2  23373  mbfimaopn2  23424  iblconst  23584  itgconst  23585  dvcnp2  23683  dvcn  23684  deg1mul3le  23876  deg1tmle  23877  dvdsq1p  23920  ig1peu  23931  ig1pdvds  23936  coeid3  23996  dgrmulc  24027  efcvx  24203  tanord  24284  logdivlti  24366  logccv  24409  recxpcl  24421  cxpeq  24498  ang180  24544  isosctrlem2  24549  cxp2lim  24703  amgm  24717  muval1  24859  dvdssqf  24864  mumullem2  24906  mumul  24907  bcmono  25002  lgsfcl2  25028  lgsdilem  25049  lgsdirprm  25056  lgsdir  25057  lgsdi  25059  lgsne0  25060  padicabv  25319  brbtwn2  25785  colinearalglem1  25786  colinearalg  25790  axcgrtr  25795  axsegconlem8  25804  axsegconlem9  25805  axsegconlem10  25806  axcontlem8  25851  axcontlem10  25853  vtxdlfuhgr1v  26375  umgr2wlk  26845  clwwlksfo  26918  clwwlksext2edg  26923  erclwwlkssym  26935  erclwwlksnsym  26947  clwlksf1clwwlklem  26968  numclwwlk2lem1  27235  numclwwlk5  27246  frgrregord13  27254  nvmul0or  27505  ipval2lem2  27559  lnomul  27615  shless  28218  shlej1  28219  pjspansn  28436  hoadddi  28662  kbmul  28814  homco2  28836  kbass2  28976  eliccelico  29539  elicoelioo  29540  iocinioc2  29541  iocinif  29543  xrge0adddir  29692  xrge0npcan  29694  archiabl  29752  ress1r  29789  rhmdvdsr  29818  pstmfval  29939  fmcncfil  29977  zrhnm  30013  qqhnm  30034  measvunilem  30275  volfiniune  30293  dya2iocnrect  30343  sibfinima  30401  probun  30481  probinc  30483  cndprob01  30497  bnj517  30955  bnj594  30982  pconnpi1  31219  cvmsss2  31256  mrsubcv  31407  msubvrs  31457  dvdspw  31636  br6  31647  br4  31648  frrlem4  31783  nosep1o  31832  nosepssdm  31836  nolt02olem  31844  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  nosupbnd2  31862  noetalem2  31864  cgrcomim  32096  cgrtriv  32109  cgrextend  32115  segconeq  32117  btwntriv2  32119  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  trisegint  32135  cgrsub  32152  cgrxfr  32162  btwnxfr  32163  lineext  32183  btwnconn1lem13  32206  btwnconn1lem14  32207  btwnconn3  32210  segcon2  32212  brsegle  32215  brsegle2  32216  segletr  32221  segleantisym  32222  seglelin  32223  outsideofeu  32238  lineunray  32254  lineelsb2  32255  ivthALT  32330  lindsenlbs  33404  areacirc  33505  cocanfo  33512  upixp  33524  ismtyima  33602  rrndstprj2  33630  zerdivemp1x  33746  lsatfixedN  34296  lssat  34303  eqlkr  34386  eqlkr2  34387  lkrlsp  34389  lshpkrlem4  34400  opposet  34468  cvrcon3b  34564  cvrcmp  34570  atlen0  34597  atnle  34604  atlatmstc  34606  cvlatexch3  34625  cvlsupr2  34630  hlsupr2  34673  hlrelat2  34689  cvrexchlem  34705  lnnat  34713  atcvrj2b  34718  atle  34722  atexchcvrN  34726  atbtwn  34732  athgt  34742  3dimlem3  34747  3dim1  34753  1cvratlt  34760  1cvrjat  34761  ps-1  34763  ps-2  34764  3atlem3  34771  3atlem5  34773  3atlem7  34775  llni  34794  llni2  34798  atcvrlln2  34805  llnexatN  34807  llncmp  34808  2llnmat  34810  2at0mat0  34811  lplni  34818  lplnnle2at  34827  2atnelpln  34830  lplnllnneN  34842  llncvrlpln2  34843  2lplnmN  34845  2llnmj  34846  lplncmp  34848  lplnexatN  34849  lplnexllnN  34850  2llnm3N  34855  lvoli  34861  lvoli3  34863  islvol2aN  34878  4atlem0a  34879  4atlem3  34882  4atlem3a  34883  4atlem4a  34885  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  4atlem10b  34891  4atlem11  34895  4atlem12  34898  lplncvrlvol2  34901  lvolcmp  34903  2lplnmj  34908  islinei  35026  pmapglbx  35055  linepmap  35061  lneq2at  35064  lnjatN  35066  lncvrat  35068  lncmp  35069  2llnma3r  35074  elpaddatriN  35089  elpaddat  35090  paddcom  35099  paddss1  35103  paddss2  35104  paddss12  35105  paddasslem6  35111  paddasslem7  35112  paddasslem8  35113  paddasslem9  35114  paddasslem15  35120  pmodlem2  35133  pmodl42N  35137  pmapjoin  35138  llnmod1i2  35146  2polcon4bN  35204  polcon2bN  35206  poml4N  35239  poml6N  35241  osumcllem1N  35242  osumcllem2N  35243  osumcllem11N  35252  osumclN  35253  pmapojoinN  35254  pexmidlem2N  35257  pexmidlem3N  35258  pexmidlem4N  35259  pexmidlem6N  35261  pexmidlem7N  35262  pl42lem2N  35266  pl42lem3N  35267  pl42lem4N  35268  pl42N  35269  lhpexle2lem  35295  lhpexle3lem  35297  lhpexle3  35298  lhpmcvr3  35311  lhp2at0nle  35321  lhprelat3N  35326  4atex  35362  4atex2  35363  lauteq  35381  lautco  35383  ltrncoidN  35414  ltrneq2  35434  ltrnnidn  35461  ltrnideq  35462  trlnid  35466  ltrnatlw  35470  trlnle  35473  trlval3  35474  trlval4  35475  cdlemc  35484  cdlemd5  35489  cdlemd9  35493  ltrneq3  35495  cdleme0moN  35512  cdleme20  35612  cdleme21j  35624  cdleme21  35625  cdleme27cl  35654  cdlemefrs29bpre0  35684  cdlemefs27cl  35701  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme32d  35732  cdleme32f  35734  cdleme32le  35735  cdleme35h2  35745  cdleme38n  35752  cdleme40m  35755  cdleme41snaw  35764  cdleme42ke  35773  cdleme17d3  35784  cdleme48fvg  35788  cdlemeg46fvcl  35794  cdlemeg46fgN  35822  cdleme48gfv1  35824  cdleme48fgv  35826  cdleme50trn3  35841  trlord  35857  ltrniotavalbN  35872  cdlemb3  35894  cdlemg6c  35908  cdlemg6  35911  cdlemg7N  35914  cdlemg8c  35917  cdlemg8  35919  cdlemg11a  35925  cdlemg11b  35930  cdlemg12e  35935  cdlemg15a  35943  cdlemg15  35944  cdlemg16  35945  cdlemg16z  35947  cdlemg16zz  35948  cdlemg17dN  35951  cdlemg18a  35966  cdlemg20  35973  cdlemg22  35975  cdlemg24  35976  cdlemg37  35977  cdlemg31d  35988  cdlemg29  35993  cdlemg33b  35995  cdlemg33  35999  cdlemg38  36003  cdlemg39  36004  cdlemg40  36005  trlco  36015  trlcone  36016  cdlemg42  36017  cdlemg44b  36020  ltrncom  36026  trljco  36028  tendococl  36060  tendoplcl  36069  tendoplcom  36070  cdlemj2  36110  cdlemj3  36111  tendoid0  36113  tendoconid  36117  tendotr  36118  cdlemk25-3  36192  cdlemk26b-3  36193  cdlemk34  36198  cdlemk36  36201  cdlemk38  36203  cdlemkid4  36222  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk19x  36231  cdlemk53  36245  cdlemk55  36249  cdlemk55u  36254  cdlemk39u  36256  cdlemk19u  36258  cdlemk56  36259  tendoex  36263  cdleml3N  36266  cdleml5N  36268  tendospcanN  36312  cdlemm10N  36407  cdlemn11pre  36499  dihord2pre  36514  dihvalcqpre  36524  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihord5apre  36551  dihord  36553  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetbN  36592  dihmeetlem4preN  36595  dihmeetlem5  36597  dihmeetlem7N  36599  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem12N  36607  dihmeetlem13N  36608  dihmeetlem15N  36610  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem18N  36613  dihmeetlem19N  36614  dihmeetALTN  36616  dih1dimatlem0  36617  dihlspsnssN  36621  dihlspsnat  36622  mapdh8ad  37068  hdmap14lem14  37173  hgmapvvlem3  37217  mzprename  37312  eldioph2lem1  37323  lzunuz  37331  rencldnfi  37385  pellexlem2  37394  infmrgelbi  37442  pellfundglb  37449  pellfund14gap  37451  qirropth  37473  rmxycomplete  37482  congadd  37533  acongeq  37550  jm2.19  37560  jm2.23  37563  jm2.20nn  37564  jm2.27  37575  jm3.1  37587  aomclem6  37629  lnmepi  37655  lmhmfgsplit  37656  lmhmlnmsplit  37657  pwssplit4  37659  hbtlem2  37694  hbtlem5  37698  dgraa0p  37719  proot1hash  37778  iocunico  37796  relexpxpmin  38009  brtrclfv2  38019  ntrclsiso  38365  ntrclskb  38367  ntrclsk3  38368  k0004lem3  38447  suprnmpt  39355  wessf1ornlem  39371  projf1o  39386  snunioo2  39731  snunioo1  39738  iccintsng  39749  lptre2pt  39872  limcleqr  39876  fnlimfvre  39906  limsupgtlem  40009  volioc  40188  iblspltprt  40189  stoweidlem19  40236  stoweidlem20  40237  stoweidlem22  40239  stoweidlem28  40245  stoweidlem34  40251  stoweidlem44  40261  stoweidlem60  40277  wallispilem3  40284  fourierdlem41  40365  fourierdlem42  40366  fourierdlem49  40372  fourierdlem51  40374  fourierdlem54  40377  fourierdlem74  40397  fourierdlem97  40420  caratheodorylem2  40741  ovnsubaddlem2  40785  hspmbllem2  40841  smflimmpt  41016  smflimsupmpt  41035  smfliminfmpt  41038  fzopredsuc  41333  fzoopth  41337  iccpartigtl  41359  repswpfx  41436  lighneal  41528  oexpnegALTV  41588  oexpnegnz  41589  tgblthelfgott  41703  tgblthelfgottOLD  41709  lidldomn1  41921  ofaddmndmap  42122  lincdifsn  42213  lincellss  42215  lincresunit3lem3  42263  islindeps2  42272  lindssnlvec  42275  fdivmptf  42335  refdivmptf  42336