Theorem simplrl 776

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

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  disjxiun  5090  frpomin  6292  f1imass  7204  f1prex  7224  soisoi  7268  riota5f  7337  frxp3  8087  xpord3pred  8088  tfrlem9a  8311  oeeui  8523  oaabs2  8570  omabs  8572  naddssim  8606  omxpenlem  8998  fopwdom  9005  frfi  9176  marypha1lem  9324  ordiso2  9408  oismo  9433  wemaplem3  9441  cantnf  9590  ttrclss  9617  isinffi  9892  dfac12lem2  10043  dfac12lem3  10044  infxp  10112  infmap2  10115  infpssrlem5  10205  fin23lem11  10215  fin23lem24  10220  fin23lem26  10223  isf32lem2  10252  isf32lem4  10254  fin1a2lem13  10310  fin1a2s  10312  ttukeylem5  10411  fpwwe2lem11  10539  fpwwe2lem12  10540  wunex2  10636  tskord  10678  prlem934  10931  mulcmpblnr  10969  dedekind  11283  addrid  11300  cnegex  11301  negeu  11357  add20  11636  divdivdiv  11829  ltmul12a  11984  lediv12a  12022  cru  12124  uzwo3  12843  xleadd1a  13154  xlemul1a  13189  ixxun  13263  ixxss12  13267  elfz0ubfz0  13534  mulexpz  14011  rpexpmord  14077  leexp1a  14084  expmulnbnd  14144  swrdccatin1  14634  pfxccatin12lem3  14641  pfxccat3  14643  abs3lem  15248  rexanre  15256  cau3lem  15264  lo1bdd2  15433  o1lo1  15446  rlimclim1  15454  rlimclim  15455  lo1resb  15473  o1resb  15475  rlimcn3  15499  o1of2  15522  o1rlimmul  15528  lo1add  15536  lo1mul  15537  isercolllem1  15574  climcau  15580  summolem2  15625  summo  15626  o1fsum  15722  prodmolem2  15844  qredeu  16571  isprm5  16620  pclem  16752  pcqmul  16767  pcexp  16773  pcneg  16788  pcprmpw2  16796  pcadd  16803  prmpwdvds  16818  4sqlem13  16871  vdwlem2  16896  vdwlem7  16901  vdwlem11  16905  vdwlem12  16906  ramval  16922  ramz2  16938  ramcl  16943  prmgaplem6  16970  cshwshashlem2  17010  imasval  17417  imasdsval  17421  mreexexd  17556  issubc3  17758  idfucl  17790  funcres2c  17812  fucpropd  17889  xpcval  18085  prfval  18107  evlfcl  18130  curf12  18135  curf1cl  18136  curf2  18137  curfcl  18140  curfuncf  18146  curf2ndf  18155  hof2val  18164  hofcl  18167  hofpropd  18175  yonedalem4a  18183  yonedainv  18189  poslubmo  18317  posglbmo  18318  isipodrs  18445  acsmapd  18462  acsinfd  18464  chnpof1  18538  mgmhmeql  18626  sgrppropd  18641  ismndd  18666  mndpropd  18669  mndpsuppss  18675  mhmeql  18736  mndind  18738  frmdup3lem  18776  mhmmnd  18979  issubg4  19060  ssnmz  19080  f1otrspeq  19361  psgneu  19420  sylow2blem3  19536  lsmdisj2  19596  pj1eu  19610  efgredlem  19661  frgpuplem  19686  frgpnabl  19789  dmdprdsplitlem  19953  pgpfac1lem3  19993  pgpfaclem3  19999  ablsimpgcygd  20022  rngpropd  20094  ringpropd  20208  dvdsrtr  20288  rngcinv  20554  ringcinv  20588  islmhm2  20974  lmhmpropd  21009  prmirredlem  21411  psgndiflemA  21540  lsmcss  21631  dsmmlss  21683  uvcf1  21731  frlmup1  21737  assapropd  21811  evlslem1  22018  coe1tmmul2  22191  mamucl  22317  mamuass  22318  mamudi  22319  mamudir  22320  mamuvs1  22321  mamuvs2  22322  mamulid  22357  mamurid  22358  dmatsubcl  22414  dmatmulcl  22416  mdetunilem7  22534  mdetunilem9  22536  cramer0  22606  cpmatmcllem  22634  mat2pmatf1  22645  decpmatmul  22688  pmatcollpw1  22692  pm2mpf1lem  22710  pm2mpmhmlem2  22735  chpidmat  22763  cpmadugsumlemB  22790  cpmadugsumlemC  22791  toponmre  23009  restbas  23074  iscncl  23185  cnpdis  23209  lmcnp  23220  dishaus  23298  cmpcovf  23307  hauscmplem  23322  dfconn2  23335  clsconn  23346  2ndcctbss  23371  1stccnp  23378  islly2  23400  llyidm  23404  cldllycmp  23411  locfincmp  23442  kgentopon  23454  1stckgenlem  23469  ptpjpre1  23487  ptbasfi  23497  txcls  23520  ptpjopn  23528  xkoccn  23535  txcnp  23536  txcmpb  23560  xkoptsub  23570  xkoco2cn  23574  xkoinjcn  23603  qtopcn  23630  qtoprest  23633  regr1lem  23655  regr1lem2  23656  kqreglem1  23657  qtophmeo  23733  fgabs  23795  hauspwpwf1  23903  flimfnfcls  23944  fclscmp  23946  cnpfcf  23957  ptcmplem4  23971  ptcmplem5  23972  cnextfval  23978  cnextfun  23980  tmdgsum2  24012  tsmsval2  24046  utoptop  24150  utop3cls  24167  ismet2  24249  blin  24337  metss2lem  24427  methaus  24436  met1stc  24437  met2ndci  24438  metcnp  24457  metcnpi3  24462  metustto  24469  metustfbas  24473  nlmvscn  24603  nrginvrcn  24608  nghmcn  24661  xrsxmet  24726  reconnlem1  24743  reconn  24745  xrge0tsms  24751  xmetdcn2  24754  metdscn  24773  addcnlem  24781  mulc1cncf  24826  cncfco  24828  cnheiborlem  24881  cnheibor  24882  nmoleub2lem2  25044  ipcn  25174  iscfil3  25201  cfilfcls  25202  iscmet3  25221  caubl  25236  bcthlem5  25256  rrxdstprj1  25337  minveclem3b  25356  minveclem7  25363  pmltpc  25379  ovolshftlem1  25438  ovolscalem1  25442  ioombl1  25491  uniioombllem6  25517  dyadss  25523  dyaddisjlem  25524  dyadmax  25527  opnmbllem  25530  itg1addlem2  25626  itg2seq  25671  bddmulibl  25768  limcfval  25801  ellimc3  25808  limciun  25823  dveflem  25911  rolle  25922  dvlip2  25928  c1liplem1  25929  dvgt0lem1  25935  dvgt0  25937  dvlt0  25938  dvne0  25944  dvcnvre  25952  dvfsumrlimge0  25965  ftc1lem6  25976  itgsubst  25984  mdegmullem  26011  ply1domn  26057  fta1g  26103  fta1b  26105  dgrlem  26162  coeid  26171  plydivalg  26235  aannenlem1  26264  aalioulem6  26273  ulmcn  26336  mtestbdd  26342  abelthlem8  26377  efif1olem4  26482  chordthm  26775  xrlimcnp  26906  lgamgulmlem5  26971  isppw2  27053  fsumvma2  27153  perfectlem2  27169  lgsdilem  27263  lgsquad2lem2  27324  lgsquad3  27326  2sqlem5  27361  2sqlem9  27366  rpvmasumlem  27426  dchrisum0flb  27449  pntpbnd  27527  pntibndlem3  27531  pntlem3  27548  pntleml  27550  nosupbday  27645  noinfbday  27660  noetasuplem4  27676  noetainflem4  27680  noetalem1  27681  slerec  27761  madebdaylemlrcut  27845  bdayon  28210  n0sfincut  28283  eucliddivs  28302  remulscllem2  28404  tgjustc1  28454  tgjustc2  28455  tgbtwnconn1lem3  28553  legtrid  28570  tglinethru  28615  tglnpt2  28620  tglineintmo  28621  mirreu3  28633  perpcom  28692  footexALT  28697  footex  28700  mideu  28717  opphllem1  28726  lnopp2hpgb  28742  axsegcon  28907  axpasch  28921  axeuclidlem  28942  ecgrtg  28963  elntg  28964  eengtrkg  28966  upgr1eopALT  29097  usgredg4  29197  usgr1eop  29230  usgr1v  29236  subuhgr  29266  subumgr  29268  subusgr  29269  nbuhgr2vtx1edgb  29332  wwlksnext  29873  usgr2wspthon  29948  clwlkclwwlkf1  29992  clwwisshclwwslem  29996  n4cyclfrgr  30273  dlwwlknondlwlknonf1o  30347  vacn  30676  ubthlem1  30852  ubthlem3  30854  minvecolem7  30865  chocunii  31283  pjhthmo  31284  pjhthlem2  31374  nmopub2tALT  31891  nmfnleub2  31908  kbass5  32102  mdslmd1lem1  32307  mdslmd1lem2  32308  mdsymlem5  32389  fcobij  32707  xrofsup  32754  mgcf1o  32991  xrge0tsmsd  33049  symgcntz  33061  archiabllem2a  33170  isarchiofld  33175  gsumvsca1  33202  gsumvsca2  33203  prmidl2  33413  ssmxidl  33446  mplvrpmrhm  33595  constrelextdg2  33781  smatrcl  33830  reff  33873  ordtconnlem1  33958  qqhval2  34016  esumpcvgval  34112  imambfm  34296  ballotlemsf1o  34548  signstfvneq0  34606  pconnconn  35296  connpconn  35300  cvmliftmo  35349  cvmlift2lem10  35377  cvmlift2lem12  35379  cvmlift3lem7  35390  mrsubff1  35579  msubff1  35621  ifscgr  36109  cgrxfr  36120  btwnconn1lem13  36164  ellines  36217  weiunso  36531  weiunfr  36532  unblimceq0lem  36571  unbdqndv2  36576  irrdiff  37391  matunitlindflem1  37676  poimirlem4  37684  poimirlem13  37693  poimirlem14  37694  heicant  37715  opnmbllem0  37716  mblfinlem3  37719  itg2addnclem  37731  itg2addnc  37734  ftc1cnnc  37752  sstotbnd  37835  cntotbnd  37856  ismtyima  37863  heibor1lem  37869  heiborlem10  37880  bfp  37884  rrncmslem  37892  islshpsm  39099  lsatcmp  39122  islshpat  39136  lfl0f  39188  iscvlat2N  39443  ishlat3N  39473  3dim1  39586  islvol5  39698  lvoli2  39700  lncvrelatN  39900  lncmp  39902  paddasslem10  39948  pclfinclN  40069  pexmidlem8N  40096  idltrn  40269  cdleme42keg  40605  cdleme42mgN  40607  cdlemf2  40681  cdlemg2cex  40710  trlcoat  40842  tendoex  41094  erngdvlem4  41110  erngdvlem4-rN  41118  dialss  41165  dibglbN  41285  diblss  41289  dihlsscpre  41353  dihglblem2aN  41412  dihglblem4  41416  dihglblem5  41417  dih1dimatlem  41448  dihglblem6  41459  lcfl7N  41620  lcfrlem9  41669  mapdh9a  41908  hdmapglem7  42048  aks4d1p8  42200  isprimroot  42206  evl1gprodd  42230  hashnexinjle  42242  deg1gprod  42253  sticksstones22  42281  grpods  42307  renegeulemv  42486  sn-subeu  42545  remulinvcom  42551  imacrhmcl  42632  fidomncyc  42653  fsuppind  42708  prjspertr  42723  prjspreln0  42727  flt4lem7  42777  nna4b4nsq  42778  isnacs3  42827  nacsfix  42829  mzpsubst  42865  eldioph2lem2  42878  eldioph2  42879  eldioph2b  42880  diophin  42889  diophun  42890  rencldnfilem  42937  irrapxlem3  42941  irrapxlem5  42943  pell1234qrreccl  42971  pell1234qrmulcl  42972  pell1qrge1  42987  pell1qrgaplem  42990  monotuz  43058  monotoddzzfi  43059  acongtr  43095  acongrep  43097  jm2.26a  43117  jm2.26lem3  43118  jm2.26  43119  jm2.27b  43123  jm2.27  43125  wepwsolem  43159  fnwe2lem2  43168  hbtlem5  43245  hbt  43247  mpaaeu  43267  cantnftermord  43437  cantnfresb  43441  omabs2  43449  tfsconcatun  43454  tfsconcatfn  43455  tfsconcatfv1  43456  tfsconcatfv2  43457  tfsconcatfv  43458  tfsconcatrn  43459  naddcnff  43479  oaun3lem1  43491  rfovcnvf1od  44121  mnurndlem1  44398  fnchoice  45150  rfcnnnub  45157  disjxp1  45190  ioondisj2  45617  iccintsng  45647  fprodcn  45724  lptioo2  45755  lptioo1  45756  limclner  45773  dvdsn1add  46061  stoweidlem14  46136  stoweidlem27  46149  stoweidlem34  46156  stoweidlem49  46171  stoweidlem56  46178  fourierdlem87  46315  iundjiun  46582  ismeannd  46589  hoidmvle  46722  prproropf1olem2  47628  perfectALTVlem2  47846  mogoldbb  47909  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  grimgrtri  48073  isubgr3stgrlem6  48095  rngcinvALTV  48400  ringcinvALTV  48434  lindslinindsimp2lem5  48587  itscnhlinecirc02p  48910  toslat  49106  iinfssclem3  49181  iinfssc  49182  iinfsubc  49183  discsubc  49189  iinfconstbas  49191  imasubc3  49281  upciclem4  49294  natoppf  49354  tposcurf1  49424  fucofvalg  49443  fuco22  49464  fuco22natlem  49470  functhinclem4  49572  functhincfun  49574  arweuthinc  49654  lanfval  49738  ranfval  49739  islmd  49790  iscmd  49791