Theorem simplrl 788

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 487	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 739	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5107  frpomin  6343  f1imass  7264  f1prex  7284  soisoi  7328  riota5f  7397  frxp3  8148  xpord3pred  8149  tfrlem9a  8374  oeeui  8589  oaabs2  8636  omabs  8638  naddssim  8673  omxpenlem  9067  fopwdom  9074  frfi  9246  marypha1lem  9394  ordiso2  9478  oismo  9503  wemaplem3  9511  cantnf  9663  ttrclss  9690  isinffi  9979  dfac12lem2  10129  dfac12lem3  10130  infxp  10198  infmap2  10201  infpssrlem5  10292  fin23lem11  10302  fin23lem24  10307  fin23lem26  10310  isf32lem2  10339  isf32lem4  10341  fin1a2lem13  10397  fin1a2s  10399  ttukeylem5  10498  fpwwe2lem11  10627  fpwwe2lem12  10628  wunex2  10724  tskord  10766  prlem934  11019  mulcmpblnr  11057  dedekind  11374  addrid  11391  cnegex  11392  negeu  11448  add20  11727  divdivdiv  11917  ltmul12a  12072  lediv12a  12109  cru  12211  uzwo3  12968  xleadd1a  13280  xlemul1a  13315  ixxun  13389  ixxss12  13393  elfz0ubfz0  13662  mulexpz  14140  rpexpmord  14206  leexp1a  14213  expmulnbnd  14273  swrdccatin1  14764  pfxccatin12lem3  14771  pfxccat3  14773  abs3lem  15392  rexanre  15400  cau3lem  15408  lo1bdd2  15577  o1lo1  15590  rlimclim1  15598  rlimclim  15599  lo1resb  15617  o1resb  15619  rlimcn3  15643  o1of2  15666  o1rlimmul  15672  lo1add  15680  lo1mul  15681  isercolllem1  15718  climcau  15724  summolem2  15769  summo  15770  o1fsum  15867  prodmolem2  15991  qredeu  16717  isprm5  16767  pclem  16899  pcqmul  16914  pcexp  16920  pcneg  16935  pcprmpw2  16943  pcadd  16950  prmpwdvds  16965  4sqlem13  17018  vdwlem2  17043  vdwlem7  17048  vdwlem11  17052  vdwlem12  17053  ramval  17069  ramz2  17085  ramcl  17090  prmgaplem6  17117  cshwshashlem2  17157  imasval  17566  imasdsval  17570  mreexexd  17705  issubc3  17907  idfucl  17939  funcres2c  17961  fucpropd  18038  xpcval  18234  prfval  18256  evlfcl  18279  curf12  18284  curf1cl  18285  curf2  18286  curfcl  18289  curfuncf  18295  curf2ndf  18304  hof2val  18313  hofcl  18316  hofpropd  18324  yonedalem4a  18332  yonedainv  18338  poslubmo  18466  posglbmo  18467  isipodrs  18594  acsmapd  18611  acsinfd  18613  chnpof1  18687  mgmhmeql  18775  sgrppropd  18790  ismndd  18815  mndpropd  18818  mndpsuppss  18824  mhmeql  18886  mndind  18888  frmdup3lem  18926  mhmmnd  19131  issubg4  19213  ssnmz  19233  f1otrspeq  19518  psgneu  19577  sylow2blem3  19693  lsmdisj2  19753  pj1eu  19767  efgredlem  19818  frgpuplem  19843  frgpnabl  19946  dmdprdsplitlem  20110  pgpfac1lem3  20150  pgpfaclem3  20156  ablsimpgcygd  20179  rngpropd  20253  ringpropd  20372  dvdsrtr  20451  rngcinv  20723  ringcinv  20757  islmhm2  21140  lmhmpropd  21175  prmidl2  21447  prmirredlem  21603  psgndiflemA  21732  lsmcss  21823  dsmmlss  21875  uvcf1  21923  frlmup1  21929  assapropd  22002  evlslem1  22214  coe1tmmul2  22418  mamucl  22539  mamuass  22540  mamudi  22541  mamudir  22542  mamuvs1  22543  mamuvs2  22544  mamulid  22579  mamurid  22580  dmatsubcl  22636  dmatmulcl  22638  mdetunilem7  22756  mdetunilem9  22758  cramer0  22828  cpmatmcllem  22856  mat2pmatf1  22867  decpmatmul  22910  pmatcollpw1  22914  pm2mpf1lem  22932  pm2mpmhmlem2  22957  chpidmat  22985  cpmadugsumlemB  23012  cpmadugsumlemC  23013  toponmre  23231  restbas  23296  iscncl  23407  cnpdis  23431  lmcnp  23442  dishaus  23520  cmpcovf  23529  hauscmplem  23544  dfconn2  23557  clsconn  23568  2ndcctbss  23593  1stccnp  23600  islly2  23622  llyidm  23626  cldllycmp  23633  locfincmp  23664  kgentopon  23676  1stckgenlem  23691  ptpjpre1  23709  ptbasfi  23719  txcls  23742  ptpjopn  23750  xkoccn  23757  txcnp  23758  txcmpb  23782  xkoptsub  23792  xkoco2cn  23796  xkoinjcn  23825  qtopcn  23852  qtoprest  23855  regr1lem  23877  regr1lem2  23878  kqreglem1  23879  qtophmeo  23955  fgabs  24017  hauspwpwf1  24125  flimfnfcls  24166  fclscmp  24168  cnpfcf  24179  ptcmplem4  24193  ptcmplem5  24194  cnextfval  24200  cnextfun  24202  tmdgsum2  24234  tsmsval2  24268  utoptop  24372  utop3cls  24389  ismet2  24471  blin  24559  metss2lem  24649  methaus  24658  met1stc  24659  met2ndci  24660  metcnp  24679  metcnpi3  24684  metustto  24691  metustfbas  24695  nlmvscn  24825  nrginvrcn  24830  nghmcn  24883  xrsxmet  24948  reconnlem1  24965  reconn  24967  xrge0tsms  24973  xmetdcn2  24976  metdscn  24995  addcnlem  25003  mulc1cncf  25045  cncfco  25047  cnheiborlem  25094  cnheibor  25095  nmoleub2lem2  25256  ipcn  25386  iscfil3  25413  cfilfcls  25414  iscmet3  25433  caubl  25448  bcthlem5  25468  rrxdstprj1  25549  minveclem3b  25568  minveclem7  25575  pmltpc  25590  ovolshftlem1  25649  ovolscalem1  25653  ioombl1  25702  uniioombllem6  25728  dyadss  25734  dyaddisjlem  25735  dyadmax  25738  opnmbllem  25741  itg1addlem2  25837  itg2seq  25882  bddmulibl  25979  limcfval  26012  ellimc3  26019  limciun  26034  dveflem  26119  rolle  26130  dvlip2  26135  c1liplem1  26136  dvgt0lem1  26142  dvgt0  26144  dvlt0  26145  dvne0  26151  dvcnvre  26159  dvfsumrlimge0  26170  ftc1lem6  26181  itgsubst  26189  mdegmullem  26216  ply1domn  26262  fta1g  26308  fta1b  26310  dgrlem  26367  coeid  26376  plydivalg  26441  aannenlem1  26472  aalioulem6  26481  ulmcn  26543  mtestbdd  26549  abelthlem8  26583  efif1olem4  26691  chordthm  26983  xrlimcnp  27114  lgamgulmlem5  27178  isppw2  27260  fsumvma2  27359  perfectlem2  27375  lgsdilem  27469  lgsquad2lem2  27530  lgsquad3  27532  2sqlem5  27567  2sqlem9  27572  rpvmasumlem  27632  dchrisum0flb  27655  pntpbnd  27733  pntibndlem3  27737  pntlem3  27754  pntleml  27756  nosupbday  27850  noinfbday  27865  noetasuplem4  27881  noetainflem4  27885  noetalem1  27886  lesrec  27973  madebdaylemlrcut  28073  bdayons  28450  n0fincut  28529  eucliddivs  28550  bdayfinbndlem1  28641  remulscllem2  28675  tgjustc1  28725  tgjustc2  28726  tgbtwnconn1lem3  28824  legtrid  28841  tglinethru  28890  tglineintmo  28896  tglnpt2  28907  mirreu3  28912  perpcom  28974  footexALT  28979  footex  28982  mideu  29000  opphllem1  29009  lnopp2hpgb  29026  axsegcon  29258  axpasch  29272  axeuclidlem  29293  ecgrtg  29314  elntg  29315  eengtrkg  29317  upgr1eopALT  29448  usgredg4  29548  usgr1eop  29581  usgr1v  29587  subuhgr  29617  subumgr  29619  subusgr  29620  nbuhgr2vtx1edgb  29683  wwlksnext  30223  usgr2wspthon  30298  clwlkclwwlkf1  30342  clwwisshclwwslem  30346  n4cyclfrgr  30623  dlwwlknondlwlknonf1o  30697  vacn  31027  ubthlem1  31203  ubthlem3  31205  minvecolem7  31216  chocunii  31634  pjhthmo  31635  pjhthlem2  31725  nmopub2tALT  32242  nmfnleub2  32259  kbass5  32453  mdslmd1lem1  32658  mdslmd1lem2  32659  mdsymlem5  32740  fcobij  33046  xrofsup  33093  mgcf1o  33304  xrge0tsmsd  33374  symgcntz  33386  archiabllem2a  33495  isarchiofld  33500  gsumvsca1  33527  gsumvsca2  33528  ssmxidl  33738  mplvrpmrhm  33918  constrelextdg2  34118  smatrcl  34167  reff  34210  ordtconnlem1  34295  qqhval2  34353  esumpcvgval  34449  imambfm  34633  ballotlemsf1o  34885  signstfvneq0  34940  pconnconn  35704  connpconn  35708  cvmliftmo  35757  cvmlift2lem10  35785  cvmlift2lem12  35787  cvmlift3lem7  35798  mrsubff1  35987  msubff1  36029  ifscgr  36517  cgrxfr  36528  btwnconn1lem13  36572  ellines  36625  nmuladdss  36671  weiunso  36958  weiunfr  36959  unblimceq0lem  37076  unbdqndv2  37081  irrdiff  37951  qdiff  37952  matunitlindflem1  38248  poimirlem4  38256  poimirlem13  38265  poimirlem14  38266  heicant  38287  opnmbllem0  38288  mblfinlem3  38291  itg2addnclem  38303  itg2addnc  38306  ftc1cnnc  38324  sstotbnd  38407  cntotbnd  38428  ismtyima  38435  heibor1lem  38441  heiborlem10  38452  bfp  38456  rrncmslem  38464  islshpsm  39735  lsatcmp  39758  islshpat  39772  lfl0f  39824  iscvlat2N  40079  ishlat3N  40109  3dim1  40222  islvol5  40334  lvoli2  40336  lncvrelatN  40536  lncmp  40538  paddasslem10  40584  pclfinclN  40705  pexmidlem8N  40732  idltrn  40905  cdleme42keg  41241  cdleme42mgN  41243  cdlemf2  41317  cdlemg2cex  41346  trlcoat  41478  tendoex  41730  erngdvlem4  41746  erngdvlem4-rN  41754  dialss  41801  dibglbN  41921  diblss  41925  dihlsscpre  41989  dihglblem2aN  42048  dihglblem4  42052  dihglblem5  42053  dih1dimatlem  42084  dihglblem6  42095  lcfl7N  42256  lcfrlem9  42305  mapdh9a  42544  hdmapglem7  42684  aks4d1p8  42835  isprimroot  42841  evl1gprodd  42865  hashnexinjle  42877  deg1gprod  42888  sticksstones22  42916  grpods  42942  renegeulemv  43110  sn-subeu  43169  remulinvcom  43175  imacrhmcl  43269  fidomncyc  43286  fsuppind  43305  prjspertr  43320  prjspreln0  43324  flt4lem7  43374  nna4b4nsq  43375  isnacs3  43424  nacsfix  43426  mzpsubst  43462  eldioph2lem2  43475  eldioph2  43476  eldioph2b  43477  diophin  43486  diophun  43487  rencldnfilem  43530  irrapxlem3  43534  irrapxlem5  43536  pell1234qrreccl  43564  pell1234qrmulcl  43565  pell1qrge1  43580  pell1qrgaplem  43583  monotuz  43651  monotoddzzfi  43652  acongtr  43688  acongrep  43690  jm2.26a  43710  jm2.26lem3  43711  jm2.26  43712  jm2.27b  43716  jm2.27  43718  wepwsolem  43752  fnwe2lem2  43761  hbtlem5  43838  hbt  43840  mpaaeu  43860  cantnftermord  44030  cantnfresb  44034  omabs2  44042  tfsconcatun  44047  tfsconcatfn  44048  tfsconcatfv1  44049  tfsconcatfv2  44050  tfsconcatfv  44051  tfsconcatrn  44052  naddcnff  44072  oaun3lem1  44084  rfovcnvf1od  44713  mnurndlem1  44974  fnchoice  45732  rfcnnnub  45739  disjxp1  45772  ioondisj2  46192  iccintsng  46222  fprodcn  46299  lptioo2  46330  lptioo1  46331  limclner  46348  dvdsn1add  46636  stoweidlem14  46711  stoweidlem27  46724  stoweidlem34  46731  stoweidlem49  46746  stoweidlem56  46753  fourierdlem87  46890  iundjiun  47157  ismeannd  47164  hoidmvle  47297  prproropf1olem2  48236  nprmmul2  48260  perfectALTVlem2  48470  mogoldbb  48533  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  grimgrtri  48697  isubgr3stgrlem6  48719  rngcinvALTV  49024  ringcinvALTV  49058  lindslinindsimp2lem5  49225  itscnhlinecirc02p  49548  toslat  49743  iinfssclem3  49817  iinfssc  49818  iinfsubc  49819  discsubc  49825  iinfconstbas  49827  imasubc3  49917  upciclem4  49930  natoppf  49990  tposcurf1  50060  fucofvalg  50079  fuco22  50100  fuco22natlem  50106  functhinclem4  50208  functhincfun  50210  arweuthinc  50290  lanfval  50374  ranfval  50375  islmd  50426  iscmd  50427