Theorem simplrl 786

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 486	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 737	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  disjxiun  5096  frpomin  6323  f1imass  7244  f1prex  7264  soisoi  7308  riota5f  7377  frxp3  8126  xpord3pred  8127  tfrlem9a  8352  oeeui  8567  oaabs2  8614  omabs  8616  naddssim  8651  omxpenlem  9046  fopwdom  9053  frfi  9225  marypha1lem  9376  ordiso2  9460  oismo  9485  wemaplem3  9493  cantnf  9645  ttrclss  9672  isinffi  9947  dfac12lem2  10098  dfac12lem3  10099  infxp  10167  infmap2  10170  infpssrlem5  10261  fin23lem11  10271  fin23lem24  10276  fin23lem26  10279  isf32lem2  10308  isf32lem4  10310  fin1a2lem13  10366  fin1a2s  10368  ttukeylem5  10467  fpwwe2lem11  10596  fpwwe2lem12  10597  wunex2  10693  tskord  10735  prlem934  10988  mulcmpblnr  11026  dedekind  11343  addrid  11360  cnegex  11361  negeu  11417  add20  11696  divdivdiv  11889  ltmul12a  12044  lediv12a  12082  cru  12184  uzwo3  12941  xleadd1a  13253  xlemul1a  13288  ixxun  13362  ixxss12  13366  elfz0ubfz0  13634  mulexpz  14112  rpexpmord  14178  leexp1a  14185  expmulnbnd  14245  swrdccatin1  14735  pfxccatin12lem3  14742  pfxccat3  14744  abs3lem  15349  rexanre  15357  cau3lem  15365  lo1bdd2  15534  o1lo1  15547  rlimclim1  15555  rlimclim  15556  lo1resb  15574  o1resb  15576  rlimcn3  15600  o1of2  15623  o1rlimmul  15629  lo1add  15637  lo1mul  15638  isercolllem1  15675  climcau  15681  summolem2  15726  summo  15727  o1fsum  15824  prodmolem2  15948  qredeu  16675  isprm5  16725  pclem  16857  pcqmul  16872  pcexp  16878  pcneg  16893  pcprmpw2  16901  pcadd  16908  prmpwdvds  16923  4sqlem13  16976  vdwlem2  17001  vdwlem7  17006  vdwlem11  17010  vdwlem12  17011  ramval  17027  ramz2  17043  ramcl  17048  prmgaplem6  17075  cshwshashlem2  17115  imasval  17524  imasdsval  17528  mreexexd  17663  issubc3  17865  idfucl  17897  funcres2c  17919  fucpropd  17996  xpcval  18192  prfval  18214  evlfcl  18237  curf12  18242  curf1cl  18243  curf2  18244  curfcl  18247  curfuncf  18253  curf2ndf  18262  hof2val  18271  hofcl  18274  hofpropd  18282  yonedalem4a  18290  yonedainv  18296  poslubmo  18424  posglbmo  18425  isipodrs  18552  acsmapd  18569  acsinfd  18571  chnpof1  18645  mgmhmeql  18733  sgrppropd  18748  ismndd  18773  mndpropd  18776  mndpsuppss  18782  mhmeql  18843  mndind  18845  frmdup3lem  18883  mhmmnd  19089  issubg4  19170  ssnmz  19190  f1otrspeq  19470  psgneu  19529  sylow2blem3  19645  lsmdisj2  19705  pj1eu  19719  efgredlem  19770  frgpuplem  19795  frgpnabl  19898  dmdprdsplitlem  20062  pgpfac1lem3  20102  pgpfaclem3  20108  ablsimpgcygd  20131  rngpropd  20203  ringpropd  20317  dvdsrtr  20396  rngcinv  20666  ringcinv  20700  islmhm2  21085  lmhmpropd  21120  prmirredlem  21504  psgndiflemA  21633  lsmcss  21724  dsmmlss  21776  uvcf1  21824  frlmup1  21830  assapropd  21903  evlslem1  22115  coe1tmmul2  22319  mamucl  22441  mamuass  22442  mamudi  22443  mamudir  22444  mamuvs1  22445  mamuvs2  22446  mamulid  22481  mamurid  22482  dmatsubcl  22538  dmatmulcl  22540  mdetunilem7  22658  mdetunilem9  22660  cramer0  22730  cpmatmcllem  22758  mat2pmatf1  22769  decpmatmul  22812  pmatcollpw1  22816  pm2mpf1lem  22834  pm2mpmhmlem2  22859  chpidmat  22887  cpmadugsumlemB  22914  cpmadugsumlemC  22915  toponmre  23133  restbas  23198  iscncl  23309  cnpdis  23333  lmcnp  23344  dishaus  23422  cmpcovf  23431  hauscmplem  23446  dfconn2  23459  clsconn  23470  2ndcctbss  23495  1stccnp  23502  islly2  23524  llyidm  23528  cldllycmp  23535  locfincmp  23566  kgentopon  23578  1stckgenlem  23593  ptpjpre1  23611  ptbasfi  23621  txcls  23644  ptpjopn  23652  xkoccn  23659  txcnp  23660  txcmpb  23684  xkoptsub  23694  xkoco2cn  23698  xkoinjcn  23727  qtopcn  23754  qtoprest  23757  regr1lem  23779  regr1lem2  23780  kqreglem1  23781  qtophmeo  23857  fgabs  23919  hauspwpwf1  24027  flimfnfcls  24068  fclscmp  24070  cnpfcf  24081  ptcmplem4  24095  ptcmplem5  24096  cnextfval  24102  cnextfun  24104  tmdgsum2  24136  tsmsval2  24170  utoptop  24274  utop3cls  24291  ismet2  24373  blin  24461  metss2lem  24551  methaus  24560  met1stc  24561  met2ndci  24562  metcnp  24581  metcnpi3  24586  metustto  24593  metustfbas  24597  nlmvscn  24727  nrginvrcn  24732  nghmcn  24785  xrsxmet  24850  reconnlem1  24867  reconn  24869  xrge0tsms  24875  xmetdcn2  24878  metdscn  24897  addcnlem  24905  mulc1cncf  24947  cncfco  24949  cnheiborlem  24996  cnheibor  24997  nmoleub2lem2  25158  ipcn  25288  iscfil3  25315  cfilfcls  25316  iscmet3  25335  caubl  25350  bcthlem5  25370  rrxdstprj1  25451  minveclem3b  25470  minveclem7  25477  pmltpc  25492  ovolshftlem1  25551  ovolscalem1  25555  ioombl1  25604  uniioombllem6  25630  dyadss  25636  dyaddisjlem  25637  dyadmax  25640  opnmbllem  25643  itg1addlem2  25739  itg2seq  25784  bddmulibl  25881  limcfval  25914  ellimc3  25921  limciun  25936  dveflem  26021  rolle  26032  dvlip2  26037  c1liplem1  26038  dvgt0lem1  26044  dvgt0  26046  dvlt0  26047  dvne0  26053  dvcnvre  26061  dvfsumrlimge0  26072  ftc1lem6  26083  itgsubst  26091  mdegmullem  26118  ply1domn  26164  fta1g  26210  fta1b  26212  dgrlem  26269  coeid  26278  plydivalg  26340  aannenlem1  26369  aalioulem6  26378  ulmcn  26439  mtestbdd  26445  abelthlem8  26479  efif1olem4  26587  chordthm  26879  xrlimcnp  27010  lgamgulmlem5  27074  isppw2  27156  fsumvma2  27255  perfectlem2  27271  lgsdilem  27365  lgsquad2lem2  27426  lgsquad3  27428  2sqlem5  27463  2sqlem9  27468  rpvmasumlem  27528  dchrisum0flb  27551  pntpbnd  27629  pntibndlem3  27633  pntlem3  27650  pntleml  27652  nosupbday  27746  noinfbday  27761  noetasuplem4  27777  noetainflem4  27781  noetalem1  27782  lesrec  27869  madebdaylemlrcut  27969  bdayons  28346  n0fincut  28425  eucliddivs  28446  bdayfinbndlem1  28537  remulscllem2  28571  tgjustc1  28621  tgjustc2  28622  tgbtwnconn1lem3  28720  legtrid  28737  tglinethru  28782  tglnpt2  28787  tglineintmo  28788  mirreu3  28800  perpcom  28859  footexALT  28864  footex  28867  mideu  28884  opphllem1  28893  lnopp2hpgb  28909  axsegcon  29074  axpasch  29088  axeuclidlem  29109  ecgrtg  29130  elntg  29131  eengtrkg  29133  upgr1eopALT  29264  usgredg4  29364  usgr1eop  29397  usgr1v  29403  subuhgr  29433  subumgr  29435  subusgr  29436  nbuhgr2vtx1edgb  29499  wwlksnext  30039  usgr2wspthon  30114  clwlkclwwlkf1  30158  clwwisshclwwslem  30162  n4cyclfrgr  30439  dlwwlknondlwlknonf1o  30513  vacn  30843  ubthlem1  31019  ubthlem3  31021  minvecolem7  31032  chocunii  31450  pjhthmo  31451  pjhthlem2  31541  nmopub2tALT  32058  nmfnleub2  32075  kbass5  32269  mdslmd1lem1  32474  mdslmd1lem2  32475  mdsymlem5  32556  fcobij  32872  xrofsup  32919  mgcf1o  33142  xrge0tsmsd  33214  symgcntz  33226  archiabllem2a  33335  isarchiofld  33340  gsumvsca1  33367  gsumvsca2  33368  prmidl2  33588  ssmxidl  33623  mplvrpmrhm  33805  constrelextdg2  34005  smatrcl  34054  reff  34097  ordtconnlem1  34182  qqhval2  34240  esumpcvgval  34336  imambfm  34520  ballotlemsf1o  34772  signstfvneq0  34830  pconnconn  35545  connpconn  35549  cvmliftmo  35598  cvmlift2lem10  35626  cvmlift2lem12  35628  cvmlift3lem7  35639  mrsubff1  35828  msubff1  35870  ifscgr  36358  cgrxfr  36369  btwnconn1lem13  36413  ellines  36466  weiunso  36790  weiunfr  36791  unblimceq0lem  36908  unbdqndv2  36913  irrdiff  37782  qdiff  37783  matunitlindflem1  38079  poimirlem4  38087  poimirlem13  38096  poimirlem14  38097  heicant  38118  opnmbllem0  38119  mblfinlem3  38122  itg2addnclem  38134  itg2addnc  38137  ftc1cnnc  38155  sstotbnd  38238  cntotbnd  38259  ismtyima  38266  heibor1lem  38272  heiborlem10  38283  bfp  38287  rrncmslem  38295  islshpsm  39568  lsatcmp  39591  islshpat  39605  lfl0f  39657  iscvlat2N  39912  ishlat3N  39942  3dim1  40055  islvol5  40167  lvoli2  40169  lncvrelatN  40369  lncmp  40371  paddasslem10  40417  pclfinclN  40538  pexmidlem8N  40565  idltrn  40738  cdleme42keg  41074  cdleme42mgN  41076  cdlemf2  41150  cdlemg2cex  41179  trlcoat  41311  tendoex  41563  erngdvlem4  41579  erngdvlem4-rN  41587  dialss  41634  dibglbN  41754  diblss  41758  dihlsscpre  41822  dihglblem2aN  41881  dihglblem4  41885  dihglblem5  41886  dih1dimatlem  41917  dihglblem6  41928  lcfl7N  42089  lcfrlem9  42138  mapdh9a  42377  hdmapglem7  42517  aks4d1p8  42668  isprimroot  42674  evl1gprodd  42698  hashnexinjle  42710  deg1gprod  42721  sticksstones22  42749  grpods  42775  renegeulemv  42941  sn-subeu  43000  remulinvcom  43006  imacrhmcl  43100  fidomncyc  43117  fsuppind  43136  prjspertr  43151  prjspreln0  43155  flt4lem7  43205  nna4b4nsq  43206  isnacs3  43255  nacsfix  43257  mzpsubst  43293  eldioph2lem2  43306  eldioph2  43307  eldioph2b  43308  diophin  43317  diophun  43318  rencldnfilem  43361  irrapxlem3  43365  irrapxlem5  43367  pell1234qrreccl  43395  pell1234qrmulcl  43396  pell1qrge1  43411  pell1qrgaplem  43414  monotuz  43482  monotoddzzfi  43483  acongtr  43519  acongrep  43521  jm2.26a  43541  jm2.26lem3  43542  jm2.26  43543  jm2.27b  43547  jm2.27  43549  wepwsolem  43583  fnwe2lem2  43592  hbtlem5  43669  hbt  43671  mpaaeu  43691  cantnftermord  43861  cantnfresb  43865  omabs2  43873  tfsconcatun  43878  tfsconcatfn  43879  tfsconcatfv1  43880  tfsconcatfv2  43881  tfsconcatfv  43882  tfsconcatrn  43883  naddcnff  43903  oaun3lem1  43915  rfovcnvf1od  44544  mnurndlem1  44821  fnchoice  45573  rfcnnnub  45580  disjxp1  45613  ioondisj2  46033  iccintsng  46063  fprodcn  46140  lptioo2  46171  lptioo1  46172  limclner  46189  dvdsn1add  46477  stoweidlem14  46552  stoweidlem27  46565  stoweidlem34  46572  stoweidlem49  46587  stoweidlem56  46594  fourierdlem87  46731  iundjiun  46998  ismeannd  47005  hoidmvle  47138  prproropf1olem2  48074  nprmmul2  48098  perfectALTVlem2  48308  mogoldbb  48371  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  grimgrtri  48535  isubgr3stgrlem6  48557  rngcinvALTV  48862  ringcinvALTV  48896  lindslinindsimp2lem5  49048  itscnhlinecirc02p  49371  toslat  49567  iinfssclem3  49641  iinfssc  49642  iinfsubc  49643  discsubc  49649  iinfconstbas  49651  imasubc3  49741  upciclem4  49754  natoppf  49814  tposcurf1  49884  fucofvalg  49903  fuco22  49924  fuco22natlem  49930  functhinclem4  50032  functhincfun  50034  arweuthinc  50114  lanfval  50198  ranfval  50199  islmd  50250  iscmd  50251