Theorem simplrl 777

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  5144  frpomin  6362  f1imass  7283  f1prex  7303  soisoi  7347  riota5f  7415  frxp3  8174  xpord3pred  8175  tfrlem9a  8424  oeeui  8638  oaabs2  8685  omabs  8687  naddssim  8721  omxpenlem  9111  fopwdom  9118  frfi  9318  marypha1lem  9470  ordiso2  9552  oismo  9577  wemaplem3  9585  cantnf  9730  ttrclss  9757  isinffi  10029  dfac12lem2  10182  dfac12lem3  10183  infxp  10251  infmap2  10254  infpssrlem5  10344  fin23lem11  10354  fin23lem24  10359  fin23lem26  10362  isf32lem2  10391  isf32lem4  10393  fin1a2lem13  10449  fin1a2s  10451  ttukeylem5  10550  fpwwe2lem11  10678  fpwwe2lem12  10679  wunex2  10775  tskord  10817  prlem934  11070  mulcmpblnr  11108  dedekind  11421  addrid  11438  cnegex  11439  negeu  11495  add20  11772  divdivdiv  11965  ltmul12a  12120  lediv12a  12158  cru  12255  uzwo3  12982  xleadd1a  13291  xlemul1a  13326  ixxun  13399  ixxss12  13403  elfz0ubfz0  13668  mulexpz  14139  rpexpmord  14204  leexp1a  14211  expmulnbnd  14270  swrdccatin1  14759  pfxccatin12lem3  14766  pfxccat3  14768  abs3lem  15373  rexanre  15381  cau3lem  15389  lo1bdd2  15556  o1lo1  15569  rlimclim1  15577  rlimclim  15578  lo1resb  15596  o1resb  15598  rlimcn3  15622  o1of2  15645  o1rlimmul  15651  lo1add  15659  lo1mul  15660  isercolllem1  15697  climcau  15703  summolem2  15748  summo  15749  o1fsum  15845  prodmolem2  15967  qredeu  16691  isprm5  16740  pclem  16871  pcqmul  16886  pcexp  16892  pcneg  16907  pcprmpw2  16915  pcadd  16922  prmpwdvds  16937  4sqlem13  16990  vdwlem2  17015  vdwlem7  17020  vdwlem11  17024  vdwlem12  17025  ramval  17041  ramz2  17057  ramcl  17062  prmgaplem6  17089  cshwshashlem2  17130  imasval  17557  imasdsval  17561  mreexexd  17692  issubc3  17899  idfucl  17931  funcres2c  17954  fucpropd  18033  xpcval  18232  prfval  18254  evlfcl  18278  curf12  18283  curf1cl  18284  curf2  18285  curfcl  18288  curfuncf  18294  curf2ndf  18303  hof2val  18312  hofcl  18315  hofpropd  18323  yonedalem4a  18331  yonedainv  18337  poslubmo  18468  posglbmo  18469  isipodrs  18594  acsmapd  18611  acsinfd  18613  mgmhmeql  18741  sgrppropd  18756  ismndd  18781  mndpropd  18784  mndpsuppss  18790  mhmeql  18851  mndind  18853  frmdup3lem  18891  mhmmnd  19094  issubg4  19175  ssnmz  19196  f1otrspeq  19479  psgneu  19538  sylow2blem3  19654  lsmdisj2  19714  pj1eu  19728  efgredlem  19779  frgpuplem  19804  frgpnabl  19907  dmdprdsplitlem  20071  pgpfac1lem3  20111  pgpfaclem3  20117  ablsimpgcygd  20140  rngpropd  20191  ringpropd  20301  dvdsrtr  20384  rngcinv  20653  ringcinv  20687  islmhm2  21054  lmhmpropd  21089  prmirredlem  21500  psgndiflemA  21636  lsmcss  21727  dsmmlss  21781  uvcf1  21829  frlmup1  21835  assapropd  21909  evlslem1  22123  coe1tmmul2  22294  mamucl  22420  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  mamulid  22462  mamurid  22463  dmatsubcl  22519  dmatmulcl  22521  mdetunilem7  22639  mdetunilem9  22641  cramer0  22711  cpmatmcllem  22739  mat2pmatf1  22750  decpmatmul  22793  pmatcollpw1  22797  pm2mpf1lem  22815  pm2mpmhmlem2  22840  chpidmat  22868  cpmadugsumlemB  22895  cpmadugsumlemC  22896  toponmre  23116  restbas  23181  iscncl  23292  cnpdis  23316  lmcnp  23327  dishaus  23405  cmpcovf  23414  hauscmplem  23429  dfconn2  23442  clsconn  23453  2ndcctbss  23478  1stccnp  23485  islly2  23507  llyidm  23511  cldllycmp  23518  locfincmp  23549  kgentopon  23561  1stckgenlem  23576  ptpjpre1  23594  ptbasfi  23604  txcls  23627  ptpjopn  23635  xkoccn  23642  txcnp  23643  txcmpb  23667  xkoptsub  23677  xkoco2cn  23681  xkoinjcn  23710  qtopcn  23737  qtoprest  23740  regr1lem  23762  regr1lem2  23763  kqreglem1  23764  qtophmeo  23840  fgabs  23902  hauspwpwf1  24010  flimfnfcls  24051  fclscmp  24053  cnpfcf  24064  ptcmplem4  24078  ptcmplem5  24079  cnextfval  24085  cnextfun  24087  tmdgsum2  24119  tsmsval2  24153  utoptop  24258  utop3cls  24275  ismet2  24358  blin  24446  metss2lem  24539  methaus  24548  met1stc  24549  met2ndci  24550  metcnp  24569  metcnpi3  24574  metustto  24581  metustfbas  24585  nlmvscn  24723  nrginvrcn  24728  nghmcn  24781  xrsxmet  24844  reconnlem1  24861  reconn  24863  xrge0tsms  24869  xmetdcn2  24872  metdscn  24891  addcnlem  24899  mulc1cncf  24944  cncfco  24946  cnheiborlem  24999  cnheibor  25000  nmoleub2lem2  25162  ipcn  25293  iscfil3  25320  cfilfcls  25321  iscmet3  25340  caubl  25355  bcthlem5  25375  rrxdstprj1  25456  minveclem3b  25475  minveclem7  25482  pmltpc  25498  ovolshftlem1  25557  ovolscalem1  25561  ioombl1  25610  uniioombllem6  25636  dyadss  25642  dyaddisjlem  25643  dyadmax  25646  opnmbllem  25649  itg1addlem2  25745  itg2seq  25791  bddmulibl  25888  limcfval  25921  ellimc3  25928  limciun  25943  dveflem  26031  rolle  26042  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  dvgt0  26057  dvlt0  26058  dvne0  26064  dvcnvre  26072  dvfsumrlimge0  26085  ftc1lem6  26096  itgsubst  26104  mdegmullem  26131  ply1domn  26177  fta1g  26223  fta1b  26225  dgrlem  26282  coeid  26291  plydivalg  26355  aannenlem1  26384  aalioulem6  26393  ulmcn  26456  mtestbdd  26462  abelthlem8  26497  efif1olem4  26601  chordthm  26894  xrlimcnp  27025  lgamgulmlem5  27090  isppw2  27172  fsumvma2  27272  perfectlem2  27288  lgsdilem  27382  lgsquad2lem2  27443  lgsquad3  27445  2sqlem5  27480  2sqlem9  27485  rpvmasumlem  27545  dchrisum0flb  27568  pntpbnd  27646  pntibndlem3  27650  pntlem3  27667  pntleml  27669  nosupbday  27764  noinfbday  27779  noetasuplem4  27795  noetainflem4  27799  noetalem1  27800  slerec  27878  madebdaylemlrcut  27951  remulscllem2  28447  tgjustc1  28497  tgjustc2  28498  tgbtwnconn1lem3  28596  legtrid  28613  tglinethru  28658  tglnpt2  28663  tglineintmo  28664  mirreu3  28676  perpcom  28735  footexALT  28740  footex  28743  mideu  28760  opphllem1  28769  lnopp2hpgb  28785  axsegcon  28956  axpasch  28970  axeuclidlem  28991  ecgrtg  29012  elntg  29013  eengtrkg  29015  upgr1eopALT  29148  usgredg4  29248  usgr1eop  29281  usgr1v  29287  subuhgr  29317  subumgr  29319  subusgr  29320  nbuhgr2vtx1edgb  29383  wwlksnext  29922  usgr2wspthon  29994  clwlkclwwlkf1  30038  clwwisshclwwslem  30042  n4cyclfrgr  30319  dlwwlknondlwlknonf1o  30393  vacn  30722  ubthlem1  30898  ubthlem3  30900  minvecolem7  30911  chocunii  31329  pjhthmo  31330  pjhthlem2  31420  nmopub2tALT  31937  nmfnleub2  31954  kbass5  32148  mdslmd1lem1  32353  mdslmd1lem2  32354  mdsymlem5  32435  fcobij  32739  xrofsup  32777  mgcf1o  32977  xrge0tsmsd  33047  symgcntz  33087  archiabllem2a  33183  gsumvsca1  33214  gsumvsca2  33215  isarchiofld  33326  prmidl2  33448  ssmxidl  33481  constrelextdg2  33751  smatrcl  33756  reff  33799  ordtconnlem1  33884  qqhval2  33944  esumpcvgval  34058  imambfm  34243  ballotlemsf1o  34494  signstfvneq0  34565  pconnconn  35215  connpconn  35219  cvmliftmo  35268  cvmlift2lem10  35296  cvmlift2lem12  35298  cvmlift3lem7  35309  mrsubff1  35498  msubff1  35540  ifscgr  36025  cgrxfr  36036  btwnconn1lem13  36080  ellines  36133  weiunso  36448  weiunfr  36449  unblimceq0lem  36488  unbdqndv2  36493  irrdiff  37308  matunitlindflem1  37602  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  heicant  37641  opnmbllem0  37642  mblfinlem3  37645  itg2addnclem  37657  itg2addnc  37660  ftc1cnnc  37678  sstotbnd  37761  cntotbnd  37782  ismtyima  37789  heibor1lem  37795  heiborlem10  37806  bfp  37810  rrncmslem  37818  islshpsm  38961  lsatcmp  38984  islshpat  38998  lfl0f  39050  iscvlat2N  39305  ishlat3N  39335  3dim1  39449  islvol5  39561  lvoli2  39563  lncvrelatN  39763  lncmp  39765  paddasslem10  39811  pclfinclN  39932  pexmidlem8N  39959  idltrn  40132  cdleme42keg  40468  cdleme42mgN  40470  cdlemf2  40544  cdlemg2cex  40573  trlcoat  40705  tendoex  40957  erngdvlem4  40973  erngdvlem4-rN  40981  dialss  41028  dibglbN  41148  diblss  41152  dihlsscpre  41216  dihglblem2aN  41275  dihglblem4  41279  dihglblem5  41280  dih1dimatlem  41311  dihglblem6  41322  lcfl7N  41483  lcfrlem9  41532  mapdh9a  41771  hdmapglem7  41911  aks4d1p8  42068  isprimroot  42074  evl1gprodd  42098  hashnexinjle  42110  deg1gprod  42121  sticksstones22  42149  grpods  42175  renegeulemv  42374  sn-subeu  42432  remulinvcom  42438  sn-itrere  42474  sn-retire  42475  imacrhmcl  42500  fidomncyc  42521  fsuppind  42576  prjspertr  42591  prjspreln0  42595  flt4lem7  42645  nna4b4nsq  42646  isnacs3  42697  nacsfix  42699  mzpsubst  42735  eldioph2lem2  42748  eldioph2  42749  eldioph2b  42750  diophin  42759  diophun  42760  rencldnfilem  42807  irrapxlem3  42811  irrapxlem5  42813  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1qrge1  42857  pell1qrgaplem  42860  monotuz  42929  monotoddzzfi  42930  acongtr  42966  acongrep  42968  jm2.26a  42988  jm2.26lem3  42989  jm2.26  42990  jm2.27b  42994  jm2.27  42996  wepwsolem  43030  fnwe2lem2  43039  hbtlem5  43116  hbt  43118  mpaaeu  43138  cantnftermord  43309  cantnfresb  43313  omabs2  43321  tfsconcatun  43326  tfsconcatfn  43327  tfsconcatfv1  43328  tfsconcatfv2  43329  tfsconcatfv  43330  tfsconcatrn  43331  naddcnff  43351  oaun3lem1  43363  rfovcnvf1od  43993  mnurndlem1  44276  fnchoice  44966  rfcnnnub  44973  disjxp1  45008  ioondisj2  45445  iccintsng  45475  fprodcn  45555  lptioo2  45586  lptioo1  45587  limclner  45606  dvdsn1add  45894  stoweidlem14  45969  stoweidlem27  45982  stoweidlem34  45989  stoweidlem49  46004  stoweidlem56  46011  fourierdlem87  46148  iundjiun  46415  ismeannd  46422  hoidmvle  46555  prproropf1olem2  47428  perfectALTVlem2  47646  mogoldbb  47709  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  grimgrtri  47851  isubgr3stgrlem6  47873  rngcinvALTV  48119  ringcinvALTV  48153  lindslinindsimp2lem5  48307  itscnhlinecirc02p  48634  toslat  48770  upciclem4  48814  functhinclem4  48843