Theorem simplrl 775

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

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  disjxiun  5144  frpomin  6338  f1imass  7259  f1prex  7278  soisoi  7321  riota5f  7390  frxp3  8133  xpord3pred  8134  tfrlem9a  8382  oeeui  8598  oaabs2  8644  omabs  8646  naddssim  8680  omxpenlem  9069  fopwdom  9076  frfi  9284  marypha1lem  9424  ordiso2  9506  oismo  9531  wemaplem3  9539  cantnf  9684  ttrclss  9711  isinffi  9983  dfac12lem2  10135  dfac12lem3  10136  infxp  10206  infmap2  10209  infpssrlem5  10298  fin23lem11  10308  fin23lem24  10313  fin23lem26  10316  isf32lem2  10345  isf32lem4  10347  fin1a2lem13  10403  fin1a2s  10405  ttukeylem5  10504  fpwwe2lem11  10632  fpwwe2lem12  10633  wunex2  10729  tskord  10771  prlem934  11024  mulcmpblnr  11062  dedekind  11373  addrid  11390  cnegex  11391  negeu  11446  add20  11722  divdivdiv  11911  ltmul12a  12066  lediv12a  12103  cru  12200  uzwo3  12923  xleadd1a  13228  xlemul1a  13263  ixxun  13336  ixxss12  13340  elfz0ubfz0  13601  mulexpz  14064  rpexpmord  14129  leexp1a  14136  expmulnbnd  14194  swrdccatin1  14671  pfxccatin12lem3  14678  pfxccat3  14680  abs3lem  15281  rexanre  15289  cau3lem  15297  lo1bdd2  15464  o1lo1  15477  rlimclim1  15485  rlimclim  15486  lo1resb  15504  o1resb  15506  rlimcn3  15530  o1of2  15553  o1rlimmul  15559  lo1add  15567  lo1mul  15568  isercolllem1  15607  climcau  15613  summolem2  15658  summo  15659  o1fsum  15755  prodmolem2  15875  qredeu  16591  isprm5  16640  pclem  16767  pcqmul  16782  pcexp  16788  pcneg  16803  pcprmpw2  16811  pcadd  16818  prmpwdvds  16833  4sqlem13  16886  vdwlem2  16911  vdwlem7  16916  vdwlem11  16920  vdwlem12  16921  ramval  16937  ramz2  16953  ramcl  16958  prmgaplem6  16985  cshwshashlem2  17026  imasval  17453  imasdsval  17457  mreexexd  17588  issubc3  17795  idfucl  17827  funcres2c  17848  fucpropd  17926  xpcval  18125  prfval  18147  evlfcl  18171  curf12  18176  curf1cl  18177  curf2  18178  curfcl  18181  curfuncf  18187  curf2ndf  18196  hof2val  18205  hofcl  18208  hofpropd  18216  yonedalem4a  18224  yonedainv  18230  poslubmo  18360  posglbmo  18361  isipodrs  18486  acsmapd  18503  acsinfd  18505  sgrppropd  18618  ismndd  18643  mndpropd  18646  mhmeql  18703  mndind  18705  frmdup3lem  18743  mhmmnd  18941  issubg4  19019  ssnmz  19040  f1otrspeq  19309  psgneu  19368  sylow2blem3  19484  lsmdisj2  19544  pj1eu  19558  efgredlem  19609  frgpuplem  19634  frgpnabl  19737  dmdprdsplitlem  19901  pgpfac1lem3  19941  pgpfaclem3  19947  ablsimpgcygd  19970  ringpropd  20095  dvdsrtr  20174  islmhm2  20641  lmhmpropd  20676  prmirredlem  21033  psgndiflemA  21145  lsmcss  21236  dsmmlss  21290  uvcf1  21338  frlmup1  21344  assapropd  21417  evlslem1  21636  coe1tmmul2  21789  mamucl  21892  mamuass  21893  mamudi  21894  mamudir  21895  mamuvs1  21896  mamuvs2  21897  mamulid  21934  mamurid  21935  dmatsubcl  21991  dmatmulcl  21993  mdetunilem7  22111  mdetunilem9  22113  cramer0  22183  cpmatmcllem  22211  mat2pmatf1  22222  decpmatmul  22265  pmatcollpw1  22269  pm2mpf1lem  22287  pm2mpmhmlem2  22312  chpidmat  22340  cpmadugsumlemB  22367  cpmadugsumlemC  22368  toponmre  22588  restbas  22653  iscncl  22764  cnpdis  22788  lmcnp  22799  dishaus  22877  cmpcovf  22886  hauscmplem  22901  dfconn2  22914  clsconn  22925  2ndcctbss  22950  1stccnp  22957  islly2  22979  llyidm  22983  cldllycmp  22990  locfincmp  23021  kgentopon  23033  1stckgenlem  23048  ptpjpre1  23066  ptbasfi  23076  txcls  23099  ptpjopn  23107  xkoccn  23114  txcnp  23115  txcmpb  23139  xkoptsub  23149  xkoco2cn  23153  xkoinjcn  23182  qtopcn  23209  qtoprest  23212  regr1lem  23234  regr1lem2  23235  kqreglem1  23236  qtophmeo  23312  fgabs  23374  hauspwpwf1  23482  flimfnfcls  23523  fclscmp  23525  cnpfcf  23536  ptcmplem4  23550  ptcmplem5  23551  cnextfval  23557  cnextfun  23559  tmdgsum2  23591  tsmsval2  23625  utoptop  23730  utop3cls  23747  ismet2  23830  blin  23918  metss2lem  24011  methaus  24020  met1stc  24021  met2ndci  24022  metcnp  24041  metcnpi3  24046  metustto  24053  metustfbas  24057  nlmvscn  24195  nrginvrcn  24200  nghmcn  24253  xrsxmet  24316  reconnlem1  24333  reconn  24335  xrge0tsms  24341  xmetdcn2  24344  metdscn  24363  addcnlem  24371  mulc1cncf  24412  cncfco  24414  cnheiborlem  24461  cnheibor  24462  nmoleub2lem2  24623  ipcn  24754  iscfil3  24781  cfilfcls  24782  iscmet3  24801  caubl  24816  bcthlem5  24836  rrxdstprj1  24917  minveclem3b  24936  minveclem7  24943  pmltpc  24958  ovolshftlem1  25017  ovolscalem1  25021  ioombl1  25070  uniioombllem6  25096  dyadss  25102  dyaddisjlem  25103  dyadmax  25106  opnmbllem  25109  itg1addlem2  25205  itg2seq  25251  bddmulibl  25347  limcfval  25380  ellimc3  25387  limciun  25402  dveflem  25487  rolle  25498  dvlip2  25503  c1liplem1  25504  dvgt0lem1  25510  dvgt0  25512  dvlt0  25513  dvne0  25519  dvcnvre  25527  dvfsumrlimge0  25538  ftc1lem6  25549  itgsubst  25557  mdegmullem  25587  ply1domn  25632  fta1g  25676  fta1b  25678  dgrlem  25734  coeid  25743  plydivalg  25803  aannenlem1  25832  aalioulem6  25841  ulmcn  25902  mtestbdd  25908  abelthlem8  25942  efif1olem4  26045  chordthm  26331  xrlimcnp  26462  lgamgulmlem5  26526  isppw2  26608  fsumvma2  26706  perfectlem2  26722  lgsdilem  26816  lgsquad2lem2  26877  lgsquad3  26879  2sqlem5  26914  2sqlem9  26919  rpvmasumlem  26979  dchrisum0flb  27002  pntpbnd  27080  pntibndlem3  27084  pntlem3  27101  pntleml  27103  nosupbday  27197  noinfbday  27212  noetasuplem4  27228  noetainflem4  27232  noetalem1  27233  slerec  27309  madebdaylemlrcut  27382  tgjustc1  27715  tgjustc2  27716  tgbtwnconn1lem3  27814  legtrid  27831  tglinethru  27876  tglnpt2  27881  tglineintmo  27882  mirreu3  27894  perpcom  27953  footexALT  27958  footex  27961  mideu  27978  opphllem1  27987  lnopp2hpgb  28003  axsegcon  28174  axpasch  28188  axeuclidlem  28209  ecgrtg  28230  elntg  28231  eengtrkg  28233  upgr1eopALT  28366  usgredg4  28463  usgr1eop  28496  usgr1v  28502  subuhgr  28532  subumgr  28534  subusgr  28535  nbuhgr2vtx1edgb  28598  wwlksnext  29136  usgr2wspthon  29208  clwlkclwwlkf1  29252  clwwisshclwwslem  29256  n4cyclfrgr  29533  dlwwlknondlwlknonf1o  29607  vacn  29934  ubthlem1  30110  ubthlem3  30112  minvecolem7  30123  chocunii  30541  pjhthmo  30542  pjhthlem2  30632  nmopub2tALT  31149  nmfnleub2  31166  kbass5  31360  mdslmd1lem1  31565  mdslmd1lem2  31566  mdsymlem5  31647  fcobij  31934  xrofsup  31967  mgcf1o  32160  xrge0tsmsd  32196  symgcntz  32233  archiabllem2a  32327  gsumvsca1  32358  gsumvsca2  32359  isarchiofld  32423  prmidl2  32547  ssmxidl  32578  smatrcl  32764  reff  32807  ordtconnlem1  32892  qqhval2  32950  esumpcvgval  33064  imambfm  33249  ballotlemsf1o  33500  signstfvneq0  33571  pconnconn  34210  connpconn  34214  cvmliftmo  34263  cvmlift2lem10  34291  cvmlift2lem12  34293  cvmlift3lem7  34304  mrsubff1  34493  msubff1  34535  ifscgr  35004  cgrxfr  35015  btwnconn1lem13  35059  ellines  35112  unblimceq0lem  35370  unbdqndv2  35375  irrdiff  36195  matunitlindflem1  36472  poimirlem4  36480  poimirlem13  36489  poimirlem14  36490  heicant  36511  opnmbllem0  36512  mblfinlem3  36515  itg2addnclem  36527  itg2addnc  36530  ftc1cnnc  36548  sstotbnd  36631  cntotbnd  36652  ismtyima  36659  heibor1lem  36665  heiborlem10  36676  bfp  36680  rrncmslem  36688  islshpsm  37838  lsatcmp  37861  islshpat  37875  lfl0f  37927  iscvlat2N  38182  ishlat3N  38212  3dim1  38326  islvol5  38438  lvoli2  38440  lncvrelatN  38640  lncmp  38642  paddasslem10  38688  pclfinclN  38809  pexmidlem8N  38836  idltrn  39009  cdleme42keg  39345  cdleme42mgN  39347  cdlemf2  39421  cdlemg2cex  39450  trlcoat  39582  tendoex  39834  erngdvlem4  39850  erngdvlem4-rN  39858  dialss  39905  dibglbN  40025  diblss  40029  dihlsscpre  40093  dihglblem2aN  40152  dihglblem4  40156  dihglblem5  40157  dih1dimatlem  40188  dihglblem6  40199  lcfl7N  40360  lcfrlem9  40409  mapdh9a  40648  hdmapglem7  40788  aks4d1p8  40940  sticksstones22  40972  imacrhmcl  41086  fsuppind  41159  renegeulemv  41237  sn-subeu  41295  remulinvcom  41301  itrere  41335  retire  41336  prjspertr  41343  prjspreln0  41347  flt4lem7  41397  nna4b4nsq  41398  isnacs3  41433  nacsfix  41435  mzpsubst  41471  eldioph2lem2  41484  eldioph2  41485  eldioph2b  41486  diophin  41495  diophun  41496  rencldnfilem  41543  irrapxlem3  41547  irrapxlem5  41549  pell1234qrreccl  41577  pell1234qrmulcl  41578  pell1qrge1  41593  pell1qrgaplem  41596  monotuz  41665  monotoddzzfi  41666  acongtr  41702  acongrep  41704  jm2.26a  41724  jm2.26lem3  41725  jm2.26  41726  jm2.27b  41730  jm2.27  41732  wepwsolem  41769  fnwe2lem2  41778  hbtlem5  41855  hbt  41857  mpaaeu  41877  cantnftermord  42055  cantnfresb  42059  omabs2  42067  tfsconcatun  42072  tfsconcatfn  42073  tfsconcatfv1  42074  tfsconcatfv2  42075  tfsconcatfv  42076  tfsconcatrn  42077  naddcnff  42097  oaun3lem1  42109  rfovcnvf1od  42740  mnurndlem1  43025  fnchoice  43698  rfcnnnub  43705  disjxp1  43741  ioondisj2  44192  iccintsng  44222  fprodcn  44302  lptioo2  44333  lptioo1  44334  limclner  44353  dvdsn1add  44641  stoweidlem14  44716  stoweidlem27  44729  stoweidlem34  44736  stoweidlem49  44751  stoweidlem56  44758  fourierdlem87  44895  iundjiun  45162  ismeannd  45169  hoidmvle  45302  prproropf1olem2  46158  perfectALTVlem2  46376  mogoldbb  46439  bgoldbtbndlem2  46460  bgoldbtbndlem3  46461  mgmhmeql  46559  rngpropd  46659  rngcinv  46832  rngcinvALTV  46844  ringcinv  46883  ringcinvALTV  46907  mndpsuppss  47000  lindslinindsimp2lem5  47096  itscnhlinecirc02p  47424  toslat  47560  functhinclem4  47617