Theorem simpl2 1191

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

Assertion

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

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1185	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simpl12  1248  simpl22  1251  simpl32  1254  simp1l2  1266  simp2l2  1272  simp3l2  1278  3anandirs  1471  rspc3ev  3638  2nreu  4449  f1prex  7303  weniso  7373  ofmpteq  7719  tfisi  7879  mposn  8126  fprlem1  8323  smogt  8405  smocdmdom  8406  omeulem1  8618  nnmord  8668  nnmword  8669  naddasslem1  8730  naddasslem2  8731  difsnen  9091  enfixsn  9119  mapunen  9184  ac6sfi  9317  ordiso2  9552  wemaplem2  9584  wemapso2lem  9589  en2eqpr  10044  acndom  10088  infmap2  10254  cflim2  10300  cfsmolem  10307  coftr  10310  fin23lem26  10362  isf32lem9  10398  fin1a2lem9  10445  fin1a2lem10  10446  gchdomtri  10666  canth4  10684  gchpwdom  10707  gruima  10839  grudomon  10854  prn0  11026  distrlem4pr  11063  prlem934  11070  addcan  11442  addcan2  11443  divmulass  11942  divmulasscom  11943  ltmul1a  12113  supmul1  12234  uzsupss  12979  xaddass  13287  xleadd1a  13291  xlesubadd  13301  xmulass  13325  xlemul2a  13327  xadddilem  13332  xadddi  13333  ixxdisj  13398  ixxun  13399  ixxlb  13405  icoshftf1o  13510  icodisj  13512  ioounsn  13513  lincmb01cmp  13531  iccf1o  13532  elfz1b  13629  ssfzoulel  13795  fzoopth  13797  modmuladd  13950  modaddmulmod  13975  ltexp2a  14202  leexp2  14207  ltexp2r  14209  exple1  14212  expnlbnd2  14269  mulsubdivbinom2  14297  fun2dmnop0  14539  ccatass  14622  ccatopth  14750  pfxccatin12lem2a  14761  repswpfx  14819  repswccat  14820  cshwidxmodr  14838  2cshw  14847  repsco  14875  s2f1o  14951  limsupgle  15509  limsupgre  15513  addcn2  15626  mulcn2  15628  binomrisefac  16074  dvdsval2  16289  dvdsadd2b  16339  dvdsmod  16362  oexpneg  16378  sadass  16504  gcdass  16580  rplpwr  16591  lcmass  16647  coprmdvds2  16687  rpmulgcd2  16689  rpdvds  16693  coprmprod  16694  cncongr2  16701  rpexp  16755  prmdiveq  16819  hashgcdlem  16821  odzdvds  16828  coprimeprodsq2  16842  pythagtriplem3  16851  pythagtriplem4  16852  pcdvdsb  16902  vdwnnlem1  17028  0ram  17053  ramz2  17057  ramub1lem1  17059  mremre  17648  mrieqv2d  17683  lubss  18570  lubun  18572  clatleglb  18575  clatglbss  18576  mrelatglb  18617  isnsgrp  18748  issubmnd  18786  gsumccat  18866  frmdss2  18888  submefmnd  18920  nmzsubg  19195  ghmnsgima  19270  gsmsymgreqlem1  19462  psgnunilem4  19529  odmodnn0  19572  odnncl  19577  odmod  19578  oddvds  19579  odeq  19582  odmulgid  19586  odmulgeq  19589  odbezout  19590  odf1o1  19604  odf1o2  19605  odngen  19609  gexdvdsi  19615  pgpfi1  19627  odcau  19636  subgslw  19648  fislw  19657  lsmless1x  19676  lsmless2x  19677  lsmsubm  19685  lsmmod  19707  lsmmod2  19708  efgsfo  19771  odadd1  19880  odadd2  19881  odadd  19882  lsmcomx  19888  prdscmnd  19893  gsumconst  19966  ablsimpgfindlem1  20141  srg1zr  20232  csrgbinom  20249  ring1eq0  20311  mulgass2  20322  rngisom1  20482  rhmdvdsr  20524  cntzsubrng  20583  cntzsubr  20622  isabvd  20829  rmodislmod  20944  rmodislmodOLD  20945  0lmhm  21056  lmhmvsca  21061  reslmhm2b  21070  pwssplit1  21075  pwssplit2  21076  pwssplit3  21077  lbspss  21098  lspsnat  21164  lidldvgen  21361  xrsdsreclblem  21447  cssmre  21728  obs2ss  21766  uvcresum  21830  frlmsslsp  21833  frlmup4  21838  lindff1  21857  f1lindf  21859  lsslindf  21867  islindf4  21875  issubassa  21904  evlsval2  22128  coe1subfv  22284  coe1sclmul  22300  coe1sclmul2  22302  mpomatmul  22467  mamutpos  22479  scmatscmide  22528  mavmulsolcl  22572  mulmarep1gsum2  22595  mdetdiaglem  22619  mdetdiag  22620  mdetunilem1  22633  mdetunilem3  22635  mdetunilem9  22641  maducoeval2  22661  madurid  22665  slesolinvbi  22702  cramerimplem1  22704  cramerlem1  22708  cramer  22712  cpmatel2  22734  m2cpm  22762  m2pmfzmap  22768  m2cpminvid2lem  22775  m2cpminvid2  22776  decpmatmul  22793  pmatcollpw1lem2  22796  pmatcollpw1  22797  pmatcollpw2lem  22798  pmatcollpwfi  22803  pm2mpcl  22818  mply1topmatcl  22826  mp2pm2mplem2  22828  mp2pm2mplem4  22830  mp2pm2mplem5  22831  mp2pm2mp  22832  pm2mpghmlem2  22833  pm2mpghmlem1  22834  chfacfisfcpmat  22876  topssnei  23147  cnconst2  23306  cnpresti  23311  cnprest2  23313  cnpdis  23316  cnt0  23369  cnt1  23373  cnhaus  23377  sscmp  23428  hauscmp  23430  cnconn  23445  unconn  23452  finlocfin  23543  comppfsc  23555  kgen2ss  23578  ptpjopn  23635  prdstopn  23651  ptrescn  23662  qtopss  23738  kqfvima  23753  fbssint  23861  fbasrn  23907  filuni  23908  fmss  23969  rnelfm  23976  fmufil  23982  fmco  23984  flimss2  23995  flimss1  23996  flimrest  24006  cnpflf2  24023  flfcnp  24027  supnfcls  24043  fclsss1  24045  fclsss2  24046  isfcf  24057  subgntr  24130  opnsubg  24131  cldsubg  24134  ghmcnp  24138  ustuqtop1  24265  bldisj  24423  blgt0  24424  bl2in  24425  blss2ps  24428  blss2  24429  blssps  24449  blss  24450  xmetresbl  24462  lpbl  24531  blcld  24533  stdbdmopn  24546  metcnp3  24568  metcnp  24569  metcnp2  24570  txmetcnp  24575  blval2  24590  nmoix  24765  nmoi2  24766  nmotri  24775  metdsge  24884  metdseq0  24889  iocopnst  24983  xrhmeo  24990  nmhmcn  25166  cphsqrtcl2  25233  cphsqrtcl3  25234  cssbn  25422  pjth  25486  ovoliunlem2  25551  volun  25593  mbfimaopn2  25705  iblconst  25867  limcvallem  25920  dvfval  25946  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  deg1mul3le  26170  deg1tmle  26171  dvdsq1p  26216  idomrootle  26226  ig1peu  26228  ig1pdvds  26233  ply1term  26257  coeid3  26293  dgrmulc  26325  dvply1  26339  aaliou2  26396  efcvx  26507  tanord  26594  eflogeq  26658  logdivlti  26676  logccv  26719  recxpcl  26731  cxplea  26752  cxpeq  26814  ang180  26871  isosctrlem2  26876  cxp2lim  27034  amgm  27048  muval1  27190  dvdssqf  27195  mumullem2  27237  mumul  27238  bcmono  27335  lgsneg  27379  lgsdilem  27382  lgsdirprm  27389  lgsdir  27390  lgsdi  27392  lgsne0  27393  nolesgn2o  27730  nogesgn1o  27732  nosep1o  27740  nosep2o  27741  nosepssdm  27745  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem4  27785  noinfbnd1lem6  27787  noinfbnd2  27790  noetasuplem3  27794  noetainflem3  27798  slelss  27960  cofsslt  27966  coinitsslt  27967  cofcutrtime  27975  addsass  28052  addsdi  28195  mulsass  28206  sltmul2  28211  divsmulw  28232  brbtwn2  28934  colinearalglem1  28935  colinearalg  28939  axcgrtr  28944  axsegconlem8  28953  axsegconlem9  28954  axsegconlem10  28955  axcontlem2  28994  axcontlem10  29002  elntg2  29014  ewlkle  29637  crctcshwlkn0lem5  29843  wwlknp  29872  wwlksnext  29922  wwlksnextproplem1  29938  wspthsnwspthsnon  29945  clwlkclwwlklem3  30029  erclwwlksym  30049  erclwwlknsym  30098  upgriseupth  30235  eucrct2eupth  30273  3cyclfrgrrn  30314  numclwwlk2lem1lem  30370  numclwwlk1lem2foa  30382  frgrregord13  30424  nvmul0or  30678  ipval2lem2  30732  lnoadd  30786  lnosub  30787  lnomul  30788  shless  31387  shlej1  31388  kbmul  31983  homco2  32005  kbass2  32145  eliccelico  32785  elicoelioo  32786  iocinioc2  32787  iocinif  32789  difioo  32790  swrdrn2  32923  swrdrn3  32924  xrge0adddir  33005  xrge0npcan  33007  isarchi2  33174  archiabl  33187  pidlnz  33383  lindssn  33385  ssmxidl  33481  pstmfval  33856  fmcncfil  33891  zrhnm  33929  qqhnm  33952  nexple  33989  volfiniune  34210  dya2iocnrect  34262  probinc  34402  cndprob01  34416  signswmnd  34550  bnj517  34877  cvmsss2  35258  cvmlift2lem10  35296  br6  35736  funsseq  35748  cgrtriv  35983  5segofs  35987  btwnouttr2  36003  btwnxfr  36037  lineext  36057  btwnconn1lem13  36080  brsegle2  36090  nn0prpwlem  36304  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  lindsenlbs  37601  blbnd  37773  ismtyima  37789  rrndstprj2  37817  ghomdiv  37878  grpokerinj  37879  lsatfixedN  38990  lssat  38997  lshpkrlem4  39094  cvrcon3b  39258  atlen0  39291  atcvreq0  39295  atnle  39298  atlatmstc  39300  atlatle  39301  cvlcvr1  39320  hlsupr2  39369  hlrelat2  39385  cvrexchlem  39401  lnnat  39409  atcvrj2b  39414  3dimlem3  39443  3dim1  39449  1cvrjat  39457  llni  39490  llni2  39494  llnexatN  39503  2llnmat  39506  lplni  39514  2atnelpln  39526  llncvrlpln2  39539  2llnmj  39542  lplnexatN  39545  lplnexllnN  39546  2llnm3N  39551  lvoli  39557  lvoli3  39559  lvolnle3at  39564  islvol2aN  39574  4atlem4a  39581  4atlem4b  39582  4atlem11  39591  lplncvrlvol2  39597  2lplnmj  39604  islinei  39722  linepmap  39757  lnjatN  39762  lncvrat  39764  lncmp  39765  elpaddn0  39782  elpaddatriN  39785  elpaddat  39786  paddcom  39795  paddss2  39800  paddss12  39801  paddasslem4  39805  paddasslem9  39810  paddasslem10  39811  pmodl42N  39833  pmapjoin  39834  llnmod1i2  39842  polcon2bN  39902  pclfinclN  39932  poml4N  39935  poml6N  39937  osumcllem1N  39938  osumcllem2N  39939  osumcllem11N  39948  osumclN  39949  pmapojoinN  39950  pexmidlem2N  39953  pexmidlem3N  39954  pexmidlem4N  39955  pexmidlem6N  39957  pexmidlem7N  39958  pl42lem2N  39962  pl42lem3N  39963  pl42lem4N  39964  pl42N  39965  lhprelat3N  40022  4atex  40058  lauteq  40077  lautco  40079  ltrncoidN  40110  ltrneq2  40130  ltrnideq  40157  trlnle  40168  trlval3  40169  cdlemc  40179  cdlemd9  40188  cdlemd  40189  cdleme21j  40318  cdleme21  40319  cdleme29ex  40356  cdlemefr27cl  40385  cdlemefs27cl  40395  cdleme32d  40426  cdleme32f  40428  cdleme35h2  40439  cdleme40m  40449  cdleme17d3  40478  cdleme48fvg  40482  cdlemeg46fvcl  40488  cdlemeg46fgN  40516  cdleme48fgv  40520  cdleme50trn3  40535  cdlemb3  40588  cdlemg8  40613  cdlemg11a  40619  cdlemg15a  40637  cdlemg15  40638  cdlemg16  40639  cdlemg16z  40641  cdlemg17dN  40645  cdlemg24  40670  cdlemg37  40671  cdlemg29  40687  cdlemg33b  40689  cdlemg38  40697  cdlemg40  40699  trlco  40709  cdlemg44b  40714  ltrncom  40720  trljco  40722  tendococl  40754  tendoplcl  40763  tendoplcom  40764  cdlemj2  40804  tendoid0  40807  tendo1ne0  40810  cdlemk25-3  40886  cdlemk36  40895  cdlemkid4  40916  cdlemk19x  40925  cdlemk53  40939  cdlemk56  40953  cdleml5N  40962  tendospcanN  41005  cdlemm10N  41100  dihord6apre  41238  dihord  41246  dihmeetlem1N  41272  dihglblem2N  41276  dihmeetlem2N  41281  dihmeetbN  41285  dihmeetlem5  41290  dihmeetlem6  41291  dihmeetlem7N  41292  dihmeetlem10N  41298  dihmeetlem12N  41300  dihmeetlem16N  41304  dihmeetlem17N  41305  dihmeetlem18N  41306  dihmeetALTN  41309  dihlspsnssN  41314  dvh3dim2  41430  dvh3dim3N  41431  lcfrlem16  41540  mapdrvallem2  41627  mapdh8ad  41761  hgmapvvlem3  41907  sticksstones1  42127  sticksstones2  42128  aks6d1c6isolem1  42155  resubcan2  42394  diophrw  42746  eldioph2lem1  42747  diophrex  42762  rencldnfi  42808  pellexlem2  42817  pellqrexplicit  42864  infmrgelbi  42865  pellfundglb  42872  pellfund14gap  42874  rmxycomplete  42905  congadd  42954  acongeq  42971  jm2.19  42981  jm2.23  42984  jm2.20nn  42985  jm2.27  42996  jm3.1  43008  lnmepi  43073  lmhmlnmsplit  43075  hbtlem2  43112  dgraa0p  43137  proot1hash  43183  iocunico  43199  iocinico  43200  oasubex  43275  cantnf2  43314  onmcl  43320  omcl2  43322  nadd2rabex  43375  nadd1rabtr  43377  nadd1rabex  43379  fzunt  43444  relexpxpmin  43706  ntrclsk3  44059  grur1cld  44227  ismnu  44256  grumnudlem  44280  ismnushort  44296  rfcnnnub  44973  uzwo4  44992  wessf1ornlem  45127  supxrge  45287  infleinflem2  45320  iccintsng  45475  climsuse  45563  lptre2pt  45595  limcleqr  45599  0ellimcdiv  45604  fnlimfvre  45629  dvnprodlem1  45901  volioc  45927  stoweidlem17  45972  stoweidlem19  45974  stoweidlem20  45975  stoweidlem22  45977  stoweidlem28  45983  stoweidlem34  45989  stoweidlem44  45999  stoweidlem60  46015  wallispilem3  46022  fourierdlem42  46104  fourierdlem48  46109  fourierdlem51  46112  fourierdlem54  46115  fourierdlem74  46135  fourierdlem77  46138  fourierdlem87  46148  fourierdlem97  46158  ioorrnopnlem  46259  ovnsubaddlem2  46526  smfinflem  46772  fsupdm  46797  finfdm  46801  eluzge0nn0  47261  fzopredsuc  47272  imasetpreimafvbijlemfv  47326  lighneallem4  47534  oexpnegALTV  47601  oexpnegnz  47602  tgblthelfgott  47739  clnbgrgrim  47839  isubgr3stgrlem3  47870  rmsupp0  48212  rmsuppss  48214  lincresunit3lem3  48319  lincresunit3lem2  48325  lindssnlvec  48331  fdivmptf  48390  refdivmptf  48391  elbigolo1  48406  rrx2linest  48591  itsclc0lem1  48605  itsclc0lem2  48606  itsclc0yqsollem1  48611  itsclc0b  48621