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 483	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1185	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl12  1248  simpl22  1251  simpl32  1254  simp1l2  1266  simp2l2  1272  simp3l2  1278  3anandirs  1471  rspc3ev  3583  2nreu  4388  f1prex  7212  weniso  7281  ofmpteq  7617  tfisi  7773  mposn  8011  fprlem1  8186  smogt  8268  smocdmdom  8269  omeulem1  8484  nnmord  8534  nnmword  8535  difsnen  8918  enfixsn  8946  mapunen  9011  ac6sfi  9152  ordiso2  9372  wemaplem2  9404  wemapso2lem  9409  en2eqpr  9864  acndom  9908  infmap2  10075  cflim2  10120  cfsmolem  10127  coftr  10130  fin23lem26  10182  isf32lem9  10218  fin1a2lem9  10265  fin1a2lem10  10266  gchdomtri  10486  canth4  10504  gchpwdom  10527  gruima  10659  grudomon  10674  prn0  10846  distrlem4pr  10883  prlem934  10890  addcan  11260  addcan2  11261  divmulass  11757  divmulasscom  11758  ltmul1a  11925  supmul1  12045  uzsupss  12781  xaddass  13084  xleadd1a  13088  xlesubadd  13098  xmulass  13122  xlemul2a  13124  xadddilem  13129  xadddi  13130  ixxdisj  13195  ixxun  13196  ixxlb  13202  icoshftf1o  13307  icodisj  13309  ioounsn  13310  lincmb01cmp  13328  iccf1o  13329  elfz1b  13426  ssfzoulel  13582  modmuladd  13734  modaddmulmod  13759  ltexp2a  13985  leexp2  13990  ltexp2r  13992  exple1  13995  expnlbnd2  14050  mulsubdivbinom2  14077  fun2dmnop0  14308  ccatass  14392  ccatopth  14527  pfxccatin12lem2a  14538  repswpfx  14596  repswccat  14597  cshwidxmodr  14615  2cshw  14624  repsco  14652  s2f1o  14728  limsupgle  15285  limsupgre  15289  addcn2  15402  mulcn2  15404  binomrisefac  15851  dvdsval2  16065  dvdsadd2b  16114  dvdsmod  16137  oexpneg  16153  sadass  16277  gcdass  16354  rplpwr  16364  lcmass  16416  coprmdvds2  16456  rpmulgcd2  16458  rpdvds  16462  coprmprod  16463  cncongr2  16470  rpexp  16524  prmdiveq  16584  hashgcdlem  16586  odzdvds  16593  coprimeprodsq2  16607  pythagtriplem3  16616  pythagtriplem4  16617  pcdvdsb  16667  vdwnnlem1  16793  0ram  16818  ramz2  16822  ramub1lem1  16824  mremre  17410  mrieqv2d  17445  lubss  18328  lubun  18330  clatleglb  18333  clatglbss  18334  mrelatglb  18375  isnsgrp  18476  issubmnd  18509  gsumccat  18576  frmdss2  18598  submefmnd  18630  nmzsubg  18889  ghmnsgima  18954  gsmsymgreqlem1  19134  psgnunilem4  19201  odmodnn0  19244  odnncl  19249  odmod  19250  oddvds  19251  odeq  19254  odmulgid  19257  odmulgeq  19260  odbezout  19261  odf1o1  19273  odf1o2  19274  odngen  19278  gexdvdsi  19284  pgpfi1  19296  odcau  19305  subgslw  19317  fislw  19326  lsmless1x  19345  lsmless2x  19346  lsmsubm  19354  lsmmod  19376  lsmmod2  19377  efgsfo  19440  odadd1  19544  odadd2  19545  odadd  19546  lsmcomx  19552  prdscmnd  19557  gsumconst  19630  ablsimpgfindlem1  19805  srg1zr  19860  csrgbinom  19877  ring1eq0  19924  mulgass2  19935  rhmdvdsr  20089  cntzsubr  20162  isabvd  20186  rmodislmod  20297  rmodislmodOLD  20298  0lmhm  20408  lmhmvsca  20413  reslmhm2b  20422  pwssplit1  20427  pwssplit2  20428  pwssplit3  20429  lbspss  20450  lspsnat  20513  lidldvgen  20632  xrsdsreclblem  20750  cssmre  21004  obs2ss  21042  uvcresum  21106  frlmsslsp  21109  frlmup4  21114  lindff1  21133  f1lindf  21135  lsslindf  21143  islindf4  21151  issubassa  21179  evlsval2  21403  coe1subfv  21543  coe1sclmul  21559  coe1sclmul2  21561  mpomatmul  21701  mamutpos  21713  scmatscmide  21762  mavmulsolcl  21806  mulmarep1gsum2  21829  mdetdiaglem  21853  mdetdiag  21854  mdetunilem1  21867  mdetunilem3  21869  mdetunilem9  21875  maducoeval2  21895  madurid  21899  slesolinvbi  21936  cramerimplem1  21938  cramerlem1  21942  cramer  21946  cpmatel2  21968  m2cpm  21996  m2pmfzmap  22002  m2cpminvid2lem  22009  m2cpminvid2  22010  decpmatmul  22027  pmatcollpw1lem2  22030  pmatcollpw1  22031  pmatcollpw2lem  22032  pmatcollpwfi  22037  pm2mpcl  22052  mply1topmatcl  22060  mp2pm2mplem2  22062  mp2pm2mplem4  22064  mp2pm2mplem5  22065  mp2pm2mp  22066  pm2mpghmlem2  22067  pm2mpghmlem1  22068  chfacfisfcpmat  22110  topssnei  22381  cnconst2  22540  cnpresti  22545  cnprest2  22547  cnpdis  22550  cnt0  22603  cnt1  22607  cnhaus  22611  sscmp  22662  hauscmp  22664  cnconn  22679  unconn  22686  finlocfin  22777  comppfsc  22789  kgen2ss  22812  ptpjopn  22869  prdstopn  22885  ptrescn  22896  qtopss  22972  kqfvima  22987  fbssint  23095  fbasrn  23141  filuni  23142  fmss  23203  rnelfm  23210  fmufil  23216  fmco  23218  flimss2  23229  flimss1  23230  flimrest  23240  cnpflf2  23257  flfcnp  23261  supnfcls  23277  fclsss1  23279  fclsss2  23280  isfcf  23291  subgntr  23364  opnsubg  23365  cldsubg  23368  ghmcnp  23372  ustuqtop1  23499  bldisj  23657  blgt0  23658  bl2in  23659  blss2ps  23662  blss2  23663  blssps  23683  blss  23684  xmetresbl  23696  lpbl  23765  blcld  23767  stdbdmopn  23780  metcnp3  23802  metcnp  23803  metcnp2  23804  txmetcnp  23809  blval2  23824  nmoix  23999  nmoi2  24000  nmotri  24009  metdsge  24118  metdseq0  24123  iocopnst  24209  xrhmeo  24215  nmhmcn  24389  cphsqrtcl2  24456  cphsqrtcl3  24457  cssbn  24645  pjth  24709  ovoliunlem2  24773  volun  24815  mbfimaopn2  24927  iblconst  25088  limcvallem  25141  dvfval  25167  dvcnp2  25190  dvcn  25191  deg1mul3le  25387  deg1tmle  25388  dvdsq1p  25431  ig1peu  25442  ig1pdvds  25447  ply1term  25471  coeid3  25507  dgrmulc  25538  dvply1  25550  aaliou2  25606  efcvx  25714  tanord  25800  eflogeq  25863  logdivlti  25881  logccv  25924  recxpcl  25936  cxplea  25957  cxpeq  26016  ang180  26070  isosctrlem2  26075  cxp2lim  26232  amgm  26246  muval1  26388  dvdssqf  26393  mumullem2  26435  mumul  26436  bcmono  26531  lgsneg  26575  lgsdilem  26578  lgsdirprm  26585  lgsdir  26586  lgsdi  26588  lgsne0  26589  nolesgn2o  26925  nogesgn1o  26927  nosep1o  26935  nosep2o  26936  nosepssdm  26940  nosupres  26961  nosupbnd1lem1  26962  nosupbnd1lem4  26965  nosupbnd1lem5  26966  nosupbnd1lem6  26967  noinfres  26976  noinfbnd1lem1  26977  noinfbnd1lem4  26980  noinfbnd1lem6  26982  noinfbnd2  26985  noetasuplem3  26989  noetainflem3  26993  brbtwn2  27562  colinearalglem1  27563  colinearalg  27567  axcgrtr  27572  axsegconlem8  27581  axsegconlem9  27582  axsegconlem10  27583  axcontlem2  27622  axcontlem10  27630  elntg2  27642  ewlkle  28261  crctcshwlkn0lem5  28467  wwlknp  28496  wwlksnext  28546  wwlksnextproplem1  28562  wspthsnwspthsnon  28569  clwlkclwwlklem3  28653  erclwwlksym  28673  erclwwlknsym  28722  upgriseupth  28859  eucrct2eupth  28897  3cyclfrgrrn  28938  numclwwlk2lem1lem  28994  numclwwlk1lem2foa  29006  frgrregord13  29048  nvmul0or  29300  ipval2lem2  29354  lnoadd  29408  lnosub  29409  lnomul  29410  shless  30009  shlej1  30010  kbmul  30605  homco2  30627  kbass2  30767  eliccelico  31385  elicoelioo  31386  iocinioc2  31387  iocinif  31389  difioo  31390  swrdrn2  31513  swrdrn3  31514  xrge0adddir  31588  xrge0npcan  31590  isarchi2  31726  archiabl  31739  pidlnz  31868  lindssn  31870  ssmxidl  31939  pstmfval  32144  fmcncfil  32179  zrhnm  32217  qqhnm  32238  nexple  32275  volfiniune  32496  dya2iocnrect  32548  probinc  32688  cndprob01  32702  signswmnd  32836  bnj517  33164  cvmsss2  33535  cvmlift2lem10  33573  br6  34013  funsseq  34025  cofsslt  34184  coinitsslt  34185  cofcutrtime  34189  cgrtriv  34400  5segofs  34404  btwnouttr2  34420  btwnxfr  34454  lineext  34474  btwnconn1lem13  34497  brsegle2  34507  nn0prpwlem  34607  lindsenlbs  35885  blbnd  36058  ismtyima  36074  rrndstprj2  36102  ghomdiv  36163  grpokerinj  36164  lsatfixedN  37284  lssat  37291  lshpkrlem4  37388  cvrcon3b  37552  atlen0  37585  atcvreq0  37589  atnle  37592  atlatmstc  37594  atlatle  37595  cvlcvr1  37614  hlsupr2  37663  hlrelat2  37679  cvrexchlem  37695  lnnat  37703  atcvrj2b  37708  3dimlem3  37737  3dim1  37743  1cvrjat  37751  llni  37784  llni2  37788  llnexatN  37797  2llnmat  37800  lplni  37808  2atnelpln  37820  llncvrlpln2  37833  2llnmj  37836  lplnexatN  37839  lplnexllnN  37840  2llnm3N  37845  lvoli  37851  lvoli3  37853  lvolnle3at  37858  islvol2aN  37868  4atlem4a  37875  4atlem4b  37876  4atlem11  37885  lplncvrlvol2  37891  2lplnmj  37898  islinei  38016  linepmap  38051  lnjatN  38056  lncvrat  38058  lncmp  38059  elpaddn0  38076  elpaddatriN  38079  elpaddat  38080  paddcom  38089  paddss2  38094  paddss12  38095  paddasslem4  38099  paddasslem9  38104  paddasslem10  38105  pmodl42N  38127  pmapjoin  38128  llnmod1i2  38136  polcon2bN  38196  pclfinclN  38226  poml4N  38229  poml6N  38231  osumcllem1N  38232  osumcllem2N  38233  osumcllem11N  38242  osumclN  38243  pmapojoinN  38244  pexmidlem2N  38247  pexmidlem3N  38248  pexmidlem4N  38249  pexmidlem6N  38251  pexmidlem7N  38252  pl42lem2N  38256  pl42lem3N  38257  pl42lem4N  38258  pl42N  38259  lhprelat3N  38316  4atex  38352  lauteq  38371  lautco  38373  ltrncoidN  38404  ltrneq2  38424  ltrnideq  38451  trlnle  38462  trlval3  38463  cdlemc  38473  cdlemd9  38482  cdlemd  38483  cdleme21j  38612  cdleme21  38613  cdleme29ex  38650  cdlemefr27cl  38679  cdlemefs27cl  38689  cdleme32d  38720  cdleme32f  38722  cdleme35h2  38733  cdleme40m  38743  cdleme17d3  38772  cdleme48fvg  38776  cdlemeg46fvcl  38782  cdlemeg46fgN  38810  cdleme48fgv  38814  cdleme50trn3  38829  cdlemb3  38882  cdlemg8  38907  cdlemg11a  38913  cdlemg15a  38931  cdlemg15  38932  cdlemg16  38933  cdlemg16z  38935  cdlemg17dN  38939  cdlemg24  38964  cdlemg37  38965  cdlemg29  38981  cdlemg33b  38983  cdlemg38  38991  cdlemg40  38993  trlco  39003  cdlemg44b  39008  ltrncom  39014  trljco  39016  tendococl  39048  tendoplcl  39057  tendoplcom  39058  cdlemj2  39098  tendoid0  39101  tendo1ne0  39104  cdlemk25-3  39180  cdlemk36  39189  cdlemkid4  39210  cdlemk19x  39219  cdlemk53  39233  cdlemk56  39247  cdleml5N  39256  tendospcanN  39299  cdlemm10N  39394  dihord6apre  39532  dihord  39540  dihmeetlem1N  39566  dihglblem2N  39570  dihmeetlem2N  39575  dihmeetbN  39579  dihmeetlem5  39584  dihmeetlem6  39585  dihmeetlem7N  39586  dihmeetlem10N  39592  dihmeetlem12N  39594  dihmeetlem16N  39598  dihmeetlem17N  39599  dihmeetlem18N  39600  dihmeetALTN  39603  dihlspsnssN  39608  dvh3dim2  39724  dvh3dim3N  39725  lcfrlem16  39834  mapdrvallem2  39921  mapdh8ad  40055  hgmapvvlem3  40201  sticksstones1  40367  sticksstones2  40368  resubcan2  40639  diophrw  40851  eldioph2lem1  40852  diophrex  40867  rencldnfi  40913  pellexlem2  40922  pellqrexplicit  40969  infmrgelbi  40970  pellfundglb  40977  pellfund14gap  40979  rmxycomplete  41010  congadd  41059  acongeq  41076  jm2.19  41086  jm2.23  41089  jm2.20nn  41090  jm2.27  41101  jm3.1  41113  lnmepi  41181  lmhmlnmsplit  41183  hbtlem2  41220  dgraa0p  41245  idomrootle  41291  proot1hash  41296  iocunico  41313  iocinico  41314  omcl2  41326  fzunt  41392  relexpxpmin  41654  ntrclsk3  42009  grur1cld  42179  ismnu  42208  grumnudlem  42232  ismnushort  42248  rfcnnnub  42908  uzwo4  42929  wessf1ornlem  43057  supxrge  43220  infleinflem2  43253  iccintsng  43405  climsuse  43493  lptre2pt  43525  limcleqr  43529  0ellimcdiv  43534  fnlimfvre  43559  dvnprodlem1  43831  volioc  43857  stoweidlem17  43902  stoweidlem19  43904  stoweidlem20  43905  stoweidlem22  43907  stoweidlem28  43913  stoweidlem34  43919  stoweidlem44  43929  stoweidlem60  43945  wallispilem3  43952  fourierdlem42  44034  fourierdlem48  44039  fourierdlem51  44042  fourierdlem54  44045  fourierdlem74  44065  fourierdlem77  44068  fourierdlem87  44078  fourierdlem97  44088  ioorrnopnlem  44189  ovnsubaddlem2  44454  smfinflem  44700  eluzge0nn0  45163  fzopredsuc  45174  fzoopth  45178  imasetpreimafvbijlemfv  45213  lighneallem4  45421  oexpnegALTV  45488  oexpnegnz  45489  tgblthelfgott  45626  rmsupp0  46063  rmsuppss  46065  lincresunit3lem3  46174  lincresunit3lem2  46180  lindssnlvec  46186  fdivmptf  46246  refdivmptf  46247  elbigolo1  46262  rrx2linest  46447  itsclc0lem1  46461  itsclc0lem2  46462  itsclc0yqsollem1  46467  itsclc0b  46477