Theorem simpl1 1171

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simpl 475	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2	1	3ad2antl1 1165	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simpl11  1228  simpl21  1231  simpl31  1234  simp1l1  1246  simp2l1  1252  simp3l1  1258  3anandirs  1451  rspc3ev  3552  2nreu  4277  f1prex  6867  cocan1  6874  weniso  6932  smogt  7810  smorndom  7811  omeulem1  8011  nnmord  8061  nnmword  8062  difsnen  8397  enfixsn  8424  mapunen  8484  ac6sfi  8559  fipreima  8627  elfiun  8691  ordiso2  8776  wemaplem2  8808  wemapso  8812  en2eqpr  9229  indcardi  9263  fodomfi2  9282  iunfictbso  9336  infmap2  9440  cofsmo  9491  cfsmolem  9492  coftr  9495  fin23lem11  9539  fincssdom  9545  fin23lem26  9547  isf32lem9  9583  ac6num  9701  gchdomtri  9851  gchpwdom  9892  winainflem  9915  tskuni  10005  gruima  10024  gruf  10033  grudomon  10039  elnpi  10210  distrlem4pr  10248  prlem934  10255  addcan  10626  addcan2  10627  divmulass  11124  divmulasscom  11125  ltmul1a  11292  suprleub  11410  supmul1  11413  suprzcl  11878  uzsupss  12157  xleadd1a  12465  xlesubadd  12475  xmulasslem3  12498  xlemul2a  12501  xadddilem  12506  xadddi2  12509  ixxun  12573  icoshftf1o  12679  ioounsn  12682  snunioc  12685  lincmb01cmp  12700  iccf1o  12701  nn0p1elfzo  12898  fzofzim  12902  ltexp2a  13348  leexp2  13353  ltexp2r  13355  exple1  13358  expnlbnd2  13413  fun2dmnop0  13666  ccatass  13754  ccat2s1fvw  13804  swrdswrdlem  13889  ccatopth  13910  ccatopthOLD  13911  repswpfx  14007  cshimadifsn  14056  cshimadifsn0  14057  cshco  14063  repsco  14067  s2f1o  14143  limsupgre  14702  addcn2  14814  mulcn2  14816  ntrivcvgmul  15121  binomrisefac  15259  dvdsmodexp  15478  dvdsadd2b  15519  dvdsmod  15541  oexpneg  15557  sadass  15683  gcdass  15754  rplpwr  15766  rppwr  15767  lcmfunsnlem1  15840  coprmdvds2  15857  rpmulgcd2  15859  qredeq  15860  rpdvds  15863  cncongr2  15871  rpexp  15923  prmdiveq  15982  hashgcdlem  15984  odzdvds  15991  modprmn0modprm0  16003  coprimeprodsq2  16005  pythagtriplem3  16014  pcdvdsb  16064  pcgcd1  16072  qexpz  16096  pockthg  16101  vdwnnlem1  16190  0ram  16215  ramz2  16219  lubss  17592  lubun  17594  clatleglb  17597  clatglbss  17598  mrelatglb  17655  isnsgrp  17759  issubmnd  17789  ress0g  17790  gsumccat  17849  frmdss2  17872  mulgneg  18034  mulgdirlem  18045  submmulg  18058  subgmulg  18080  nmzsubg  18107  ghmmulg  18144  gsmsymgreqlem1  18322  pmtrfb  18357  psgnunilem4  18390  odmodnn0  18433  odnncl  18438  odmod  18439  odmulgid  18445  odmulgeq  18448  odf1o1  18461  odf1o2  18462  odngen  18466  gexdvdsi  18472  pgpfi1  18484  odcau  18493  subgslw  18505  fislw  18514  lsmssv  18532  lsmless1x  18533  lsmless2x  18534  lsmsubm  18542  lsmmod  18562  lsmmod2  18563  efgred  18637  cntzcmn  18721  ghmplusg  18725  odadd1  18727  odadd2  18728  odadd  18729  lsmcomx  18735  gsumconst  18810  srg1zr  19005  ring1eq0  19066  mulgass2  19077  isabvd  19316  rmodislmodlem  19426  rmodislmod  19427  lssintcl  19461  0lmhm  19537  lmhmvsca  19542  reslmhm2b  19551  pwssplit1  19556  pwssplit3  19558  lspfixed  19625  lspsnat  19642  lidldvgen  19752  issubassa  19821  evlsval2  20016  psrplusgpropd  20110  coe1subfv  20140  coe1mul2  20143  xrsdsreclblem  20296  regsumsupp  20471  obselocv  20577  uvcresum  20642  frlmsslsp  20645  frlmup4  20650  lindff1  20669  f1lindf  20671  lsslindf  20679  islindf4  20687  lbslcic  20690  mhmvlin  20713  mpomatmul  20762  mamutpos  20774  scmatscmide  20823  mavmulsolcl  20867  marrepcl  20880  mdetdiag  20915  mdetunilem1  20928  mdetunilem3  20930  mdetunilem7  20934  mdetunilem9  20936  mdetmul  20939  slesolinvbi  20997  m2pmfzmap  21062  pmatcollpwlem  21095  pmatcollpw  21096  mp2pm2mplem4  21124  chpdmatlem3  21155  chfacfisfcpmat  21170  chfacfscmulgsum  21175  chfacfpmmulgsum  21179  chfacfpmmulgsum2  21180  cayhamlem1  21181  cpmidpmatlem2  21186  cpmadugsumlemB  21189  cpmadugsumlemC  21190  cpmadugsumlemF  21191  riinopn  21223  neiint  21419  topssnei  21439  restntr  21497  iscnp4  21578  cnconst2  21598  cnrest2  21601  cnprest2  21605  cnpdis  21608  cnt0  21661  cnt1  21665  cnhaus  21669  ordthauslem  21698  cncmp  21707  fiuncmp  21719  sscmp  21720  hauscmp  21722  cnconn  21737  unconn  21744  nlly2i  21791  llynlly  21792  nllyidm  21804  finlocfin  21835  ptrescn  21954  xkococnlem  21974  qtopss  22030  kqfvima  22045  r0cld  22053  ordthmeolem  22116  fbssint  22153  fmf  22260  fmss  22261  elfm  22262  rnelfmlem  22267  rnelfm  22268  fmco  22276  flimss2  22287  flimss1  22288  flimrest  22298  flftg  22311  cnpflf2  22315  cnpflf  22316  flfcnp  22319  supnfcls  22335  fclsss1  22337  fclsss2  22338  fcfnei  22350  fcfelbas  22351  cnpfcfi  22355  subgntr  22421  opnsubg  22422  cldsubg  22425  ghmcnp  22429  utop2nei  22565  neipcfilu  22611  bldisj  22714  blgt0  22715  bl2in  22716  blss2ps  22719  blss2  22720  blssps  22740  blss  22741  xmetresbl  22753  lpbl  22819  blcld  22821  stdbdbl  22833  metcnp3  22856  metcnp2  22858  txmetcnp  22863  blval2  22878  nmoix  23044  nmoeq0  23051  icoopnst  23249  iocopnst  23250  xrhmeo  23256  nmhmcn  23430  cphsqrtcl2  23496  cphsqrtcl3  23497  cfil3i  23578  caublcls  23618  bcthlem5  23637  cmetcusp1  23662  cssbn  23684  rrxcph  23701  pjth  23748  ovoliunlem2  23810  volun  23852  volsup2  23912  mbfimaopn2  23964  iblconst  24124  itgconst  24125  dvcnp2  24223  dvcn  24224  deg1mul3le  24416  deg1tmle  24417  dvdsq1p  24460  ig1peu  24471  ig1pdvds  24476  coeid3  24536  dgrmulc  24567  efcvx  24743  tanord  24826  logdivlti  24907  logccv  24950  recxpcl  24962  cxpeq  25042  ang180  25096  isosctrlem2  25101  cxp2lim  25259  amgm  25273  muval1  25415  dvdssqf  25420  mumullem2  25462  mumul  25463  bcmono  25558  lgsfcl2  25584  lgsdilem  25605  lgsdirprm  25612  lgsdir  25613  lgsdi  25615  lgsne0  25616  padicabv  25911  brbtwn2  26397  colinearalglem1  26398  colinearalg  26402  axcgrtr  26407  axsegconlem8  26416  axsegconlem9  26417  axsegconlem10  26418  axcontlem8  26463  axcontlem10  26465  elntg2  26477  vtxdlfuhgr1v  26967  umgr2wlk  27458  erclwwlksym  27539  clwwlkfoOLD  27570  clwwlkfo  27575  clwwlkext2edg  27582  erclwwlknsym  27597  clwwlknon1  27628  numclwwlk2lem1  27932  numclwwlk5  27948  frgrregord13  27956  nvmul0or  28207  ipval2lem2  28261  lnomul  28317  shless  28920  shlej1  28921  pjspansn  29138  hoadddi  29364  kbmul  29516  homco2  29538  kbass2  29678  eliccelico  30255  elicoelioo  30256  iocinioc2  30257  iocinif  30259  xrge0adddir  30411  xrge0npcan  30413  archiabl  30493  ress1r  30539  rhmdvdsr  30570  pstmfval  30780  fmcncfil  30818  zrhnm  30854  qqhnm  30875  measvunilem  31116  volfiniune  31134  dya2iocnrect  31184  sibfinima  31242  probun  31323  probinc  31325  cndprob01  31339  bnj517  31804  bnj594  31831  pconnpi1  32069  cvmsss2  32106  mrsubcv  32277  msubvrs  32327  dvdspw  32502  br6  32513  br4  32514  frpomin  32599  frrlem4  32647  frrlem10  32653  fprlem1  32658  nosep1o  32707  nosepssdm  32711  nolt02olem  32719  nosupres  32728  nosupbnd1lem1  32729  nosupbnd1lem4  32732  nosupbnd1lem5  32733  nosupbnd1lem6  32734  nosupbnd2  32737  noetalem2  32739  cgrcomim  32971  cgrtriv  32984  cgrextend  32990  segconeq  32992  btwntriv2  32994  btwnintr  33001  btwnexch3  33002  btwnouttr2  33004  trisegint  33010  cgrsub  33027  cgrxfr  33037  btwnxfr  33038  lineext  33058  btwnconn1lem13  33081  btwnconn1lem14  33082  btwnconn3  33085  segcon2  33087  brsegle  33090  brsegle2  33091  segletr  33096  segleantisym  33097  seglelin  33098  outsideofeu  33113  lineunray  33129  lineelsb2  33130  ivthALT  33204  lindsenlbs  34328  areacirc  34428  cocanfo  34435  upixp  34446  ismtyima  34523  rrndstprj2  34551  zerdivemp1x  34667  lsatfixedN  35590  lssat  35597  eqlkr  35680  eqlkr2  35681  lkrlsp  35683  lshpkrlem4  35694  opposet  35762  cvrcon3b  35858  cvrcmp  35864  atlen0  35891  atnle  35898  atlatmstc  35900  cvlatexch3  35919  cvlsupr2  35924  hlsupr2  35968  hlrelat2  35984  cvrexchlem  36000  lnnat  36008  atcvrj2b  36013  atle  36017  atexchcvrN  36021  atbtwn  36027  athgt  36037  3dimlem3  36042  3dim1  36048  1cvratlt  36055  1cvrjat  36056  ps-1  36058  ps-2  36059  3atlem3  36066  3atlem5  36068  3atlem7  36070  llni  36089  llni2  36093  atcvrlln2  36100  llnexatN  36102  llncmp  36103  2llnmat  36105  2at0mat0  36106  lplni  36113  lplnnle2at  36122  2atnelpln  36125  lplnllnneN  36137  llncvrlpln2  36138  2lplnmN  36140  2llnmj  36141  lplncmp  36143  lplnexatN  36144  lplnexllnN  36145  2llnm3N  36150  lvoli  36156  lvoli3  36158  islvol2aN  36173  4atlem0a  36174  4atlem3  36177  4atlem3a  36178  4atlem4a  36180  4atlem4b  36181  4atlem4c  36182  4atlem4d  36183  4atlem10b  36186  4atlem11  36190  4atlem12  36193  lplncvrlvol2  36196  lvolcmp  36198  2lplnmj  36203  islinei  36321  pmapglbx  36350  linepmap  36356  lneq2at  36359  lnjatN  36361  lncvrat  36363  lncmp  36364  2llnma3r  36369  elpaddatriN  36384  elpaddat  36385  paddcom  36394  paddss1  36398  paddss2  36399  paddss12  36400  paddasslem6  36406  paddasslem7  36407  paddasslem8  36408  paddasslem9  36409  paddasslem15  36415  pmodlem2  36428  pmodl42N  36432  pmapjoin  36433  llnmod1i2  36441  2polcon4bN  36499  polcon2bN  36501  poml4N  36534  poml6N  36536  osumcllem1N  36537  osumcllem2N  36538  osumcllem11N  36547  osumclN  36548  pmapojoinN  36549  pexmidlem2N  36552  pexmidlem3N  36553  pexmidlem4N  36554  pexmidlem6N  36556  pexmidlem7N  36557  pl42lem2N  36561  pl42lem3N  36562  pl42lem4N  36563  pl42N  36564  lhpexle2lem  36590  lhpexle3lem  36592  lhpexle3  36593  lhpmcvr3  36606  lhp2at0nle  36616  lhprelat3N  36621  4atex  36657  4atex2  36658  lauteq  36676  lautco  36678  ltrncoidN  36709  ltrneq2  36729  ltrnnidn  36755  ltrnideq  36756  trlnid  36760  ltrnatlw  36764  trlnle  36767  trlval3  36768  trlval4  36769  cdlemc  36778  cdlemd5  36783  cdlemd9  36787  ltrneq3  36789  cdleme0moN  36806  cdleme20  36905  cdleme21j  36917  cdleme21  36918  cdleme27cl  36947  cdlemefrs29bpre0  36977  cdlemefs27cl  36994  cdlemefs32sn1aw  36995  cdleme43fsv1snlem  37001  cdleme32d  37025  cdleme32f  37027  cdleme32le  37028  cdleme35h2  37038  cdleme38n  37045  cdleme40m  37048  cdleme41snaw  37057  cdleme42ke  37066  cdleme17d3  37077  cdleme48fvg  37081  cdlemeg46fvcl  37087  cdlemeg46fgN  37115  cdleme48gfv1  37117  cdleme48fgv  37119  cdleme50trn3  37134  trlord  37150  ltrniotavalbN  37165  cdlemb3  37187  cdlemg6c  37201  cdlemg6  37204  cdlemg7N  37207  cdlemg8c  37210  cdlemg8  37212  cdlemg11a  37218  cdlemg11b  37223  cdlemg12e  37228  cdlemg15a  37236  cdlemg15  37237  cdlemg16  37238  cdlemg16z  37240  cdlemg16zz  37241  cdlemg17dN  37244  cdlemg18a  37259  cdlemg20  37266  cdlemg22  37268  cdlemg24  37269  cdlemg37  37270  cdlemg31d  37281  cdlemg29  37286  cdlemg33b  37288  cdlemg33  37292  cdlemg38  37296  cdlemg39  37297  cdlemg40  37298  trlco  37308  trlcone  37309  cdlemg42  37310  cdlemg44b  37313  ltrncom  37319  trljco  37321  tendococl  37353  tendoplcl  37362  tendoplcom  37363  cdlemj2  37403  cdlemj3  37404  tendoid0  37406  tendoconid  37410  tendotr  37411  cdlemk25-3  37485  cdlemk26b-3  37486  cdlemk34  37491  cdlemk36  37494  cdlemk38  37496  cdlemkid4  37515  cdlemk35s-id  37519  cdlemk39s-id  37521  cdlemk19x  37524  cdlemk53  37538  cdlemk55  37542  cdlemk55u  37547  cdlemk39u  37549  cdlemk19u  37551  cdlemk56  37552  tendoex  37556  cdleml3N  37559  cdleml5N  37561  tendospcanN  37604  cdlemm10N  37699  cdlemn11pre  37791  dihord2pre  37806  dihvalcqpre  37816  dihopelvalcpre  37829  dihord6apre  37837  dihord5b  37840  dihord5apre  37843  dihord  37845  dihmeetlem1N  37871  dihglblem5apreN  37872  dihglblem3N  37876  dihmeetlem2N  37880  dihglbcpreN  37881  dihmeetbN  37884  dihmeetlem4preN  37887  dihmeetlem5  37889  dihmeetlem7N  37891  dihmeetlem10N  37897  dihmeetlem11N  37898  dihmeetlem12N  37899  dihmeetlem13N  37900  dihmeetlem15N  37902  dihmeetlem16N  37903  dihmeetlem17N  37904  dihmeetlem18N  37905  dihmeetlem19N  37906  dihmeetALTN  37908  dih1dimatlem0  37909  dihlspsnssN  37913  dihlspsnat  37914  mapdh8ad  38360  hdmap14lem14  38462  hgmapvvlem3  38506  resubcan2  38649  mzprename  38741  eldioph2lem1  38752  lzunuz  38760  rencldnfi  38814  pellexlem2  38823  infmrgelbi  38871  pellfundglb  38878  pellfund14gap  38880  qirropth  38901  rmxycomplete  38910  congadd  38959  acongeq  38976  jm2.19  38986  jm2.23  38989  jm2.20nn  38990  jm2.27  39001  jm3.1  39013  aomclem6  39055  lnmepi  39081  lmhmfgsplit  39082  lmhmlnmsplit  39083  pwssplit4  39085  hbtlem2  39120  hbtlem5  39124  dgraa0p  39145  proot1hash  39196  iocunico  39213  relexpxpmin  39425  brtrclfv2  39435  ntrclsiso  39780  ntrclskb  39782  ntrclsk3  39783  k0004lem3  39862  grur1cld  39943  ismnu  39972  grumnudlem  39996  ablsimpgprmd  40050  suprnmpt  40855  wessf1ornlem  40870  projf1o  40885  snunioo1  41220  iccintsng  41231  lptre2pt  41353  limcleqr  41357  fnlimfvre  41387  limsupgtlem  41490  volioc  41688  iblspltprt  41689  stoweidlem19  41736  stoweidlem20  41737  stoweidlem22  41739  stoweidlem28  41745  stoweidlem34  41751  stoweidlem44  41761  stoweidlem60  41777  wallispilem3  41784  fourierdlem41  41865  fourierdlem42  41866  fourierdlem49  41872  fourierdlem51  41874  fourierdlem54  41877  fourierdlem74  41897  fourierdlem97  41920  caratheodorylem2  42241  ovnsubaddlem2  42285  hspmbllem2  42341  smflimmpt  42516  smflimsupmpt  42535  smfliminfmpt  42538  fzopredsuc  42930  fzoopth  42934  iccpartigtl  42956  lighneal  43145  oexpnegALTV  43211  oexpnegnz  43212  tgblthelfgott  43349  lidldomn1  43557  ofaddmndmap  43757  lincdifsn  43847  lincellss  43849  lincresunit3lem3  43897  islindeps2  43906  lindssnlvec  43909  fdivmptf  43970  refdivmptf  43971  rrx2linest  44098  itsclc0yqsollem1  44118  itsclc0b  44128  itsclquadb  44132  itscnhlinecirc02plem3  44140