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  5116  frpomin  6329  f1imass  7256  f1prex  7276  soisoi  7320  riota5f  7388  frxp3  8148  xpord3pred  8149  tfrlem9a  8398  oeeui  8612  oaabs2  8659  omabs  8661  naddssim  8695  omxpenlem  9085  fopwdom  9092  frfi  9291  marypha1lem  9443  ordiso2  9527  oismo  9552  wemaplem3  9560  cantnf  9705  ttrclss  9732  isinffi  10004  dfac12lem2  10157  dfac12lem3  10158  infxp  10226  infmap2  10229  infpssrlem5  10319  fin23lem11  10329  fin23lem24  10334  fin23lem26  10337  isf32lem2  10366  isf32lem4  10368  fin1a2lem13  10424  fin1a2s  10426  ttukeylem5  10525  fpwwe2lem11  10653  fpwwe2lem12  10654  wunex2  10750  tskord  10792  prlem934  11045  mulcmpblnr  11083  dedekind  11396  addrid  11413  cnegex  11414  negeu  11470  add20  11747  divdivdiv  11940  ltmul12a  12095  lediv12a  12133  cru  12230  uzwo3  12957  xleadd1a  13267  xlemul1a  13302  ixxun  13376  ixxss12  13380  elfz0ubfz0  13647  mulexpz  14118  rpexpmord  14184  leexp1a  14191  expmulnbnd  14251  swrdccatin1  14741  pfxccatin12lem3  14748  pfxccat3  14750  abs3lem  15355  rexanre  15363  cau3lem  15371  lo1bdd2  15538  o1lo1  15551  rlimclim1  15559  rlimclim  15560  lo1resb  15578  o1resb  15580  rlimcn3  15604  o1of2  15627  o1rlimmul  15633  lo1add  15641  lo1mul  15642  isercolllem1  15679  climcau  15685  summolem2  15730  summo  15731  o1fsum  15827  prodmolem2  15949  qredeu  16675  isprm5  16724  pclem  16856  pcqmul  16871  pcexp  16877  pcneg  16892  pcprmpw2  16900  pcadd  16907  prmpwdvds  16922  4sqlem13  16975  vdwlem2  17000  vdwlem7  17005  vdwlem11  17009  vdwlem12  17010  ramval  17026  ramz2  17042  ramcl  17047  prmgaplem6  17074  cshwshashlem2  17114  imasval  17523  imasdsval  17527  mreexexd  17658  issubc3  17860  idfucl  17892  funcres2c  17914  fucpropd  17991  xpcval  18187  prfval  18209  evlfcl  18232  curf12  18237  curf1cl  18238  curf2  18239  curfcl  18242  curfuncf  18248  curf2ndf  18257  hof2val  18266  hofcl  18269  hofpropd  18277  yonedalem4a  18285  yonedainv  18291  poslubmo  18419  posglbmo  18420  isipodrs  18545  acsmapd  18562  acsinfd  18564  mgmhmeql  18692  sgrppropd  18707  ismndd  18732  mndpropd  18735  mndpsuppss  18741  mhmeql  18802  mndind  18804  frmdup3lem  18842  mhmmnd  19045  issubg4  19126  ssnmz  19147  f1otrspeq  19426  psgneu  19485  sylow2blem3  19601  lsmdisj2  19661  pj1eu  19675  efgredlem  19726  frgpuplem  19751  frgpnabl  19854  dmdprdsplitlem  20018  pgpfac1lem3  20058  pgpfaclem3  20064  ablsimpgcygd  20087  rngpropd  20132  ringpropd  20246  dvdsrtr  20326  rngcinv  20595  ringcinv  20629  islmhm2  20994  lmhmpropd  21029  prmirredlem  21431  psgndiflemA  21559  lsmcss  21650  dsmmlss  21702  uvcf1  21750  frlmup1  21756  assapropd  21830  evlslem1  22038  coe1tmmul2  22211  mamucl  22337  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  mamulid  22377  mamurid  22378  dmatsubcl  22434  dmatmulcl  22436  mdetunilem7  22554  mdetunilem9  22556  cramer0  22626  cpmatmcllem  22654  mat2pmatf1  22665  decpmatmul  22708  pmatcollpw1  22712  pm2mpf1lem  22730  pm2mpmhmlem2  22755  chpidmat  22783  cpmadugsumlemB  22810  cpmadugsumlemC  22811  toponmre  23029  restbas  23094  iscncl  23205  cnpdis  23229  lmcnp  23240  dishaus  23318  cmpcovf  23327  hauscmplem  23342  dfconn2  23355  clsconn  23366  2ndcctbss  23391  1stccnp  23398  islly2  23420  llyidm  23424  cldllycmp  23431  locfincmp  23462  kgentopon  23474  1stckgenlem  23489  ptpjpre1  23507  ptbasfi  23517  txcls  23540  ptpjopn  23548  xkoccn  23555  txcnp  23556  txcmpb  23580  xkoptsub  23590  xkoco2cn  23594  xkoinjcn  23623  qtopcn  23650  qtoprest  23653  regr1lem  23675  regr1lem2  23676  kqreglem1  23677  qtophmeo  23753  fgabs  23815  hauspwpwf1  23923  flimfnfcls  23964  fclscmp  23966  cnpfcf  23977  ptcmplem4  23991  ptcmplem5  23992  cnextfval  23998  cnextfun  24000  tmdgsum2  24032  tsmsval2  24066  utoptop  24171  utop3cls  24188  ismet2  24270  blin  24358  metss2lem  24448  methaus  24457  met1stc  24458  met2ndci  24459  metcnp  24478  metcnpi3  24483  metustto  24490  metustfbas  24494  nlmvscn  24624  nrginvrcn  24629  nghmcn  24682  xrsxmet  24747  reconnlem1  24764  reconn  24766  xrge0tsms  24772  xmetdcn2  24775  metdscn  24794  addcnlem  24802  mulc1cncf  24847  cncfco  24849  cnheiborlem  24902  cnheibor  24903  nmoleub2lem2  25065  ipcn  25196  iscfil3  25223  cfilfcls  25224  iscmet3  25243  caubl  25258  bcthlem5  25278  rrxdstprj1  25359  minveclem3b  25378  minveclem7  25385  pmltpc  25401  ovolshftlem1  25460  ovolscalem1  25464  ioombl1  25513  uniioombllem6  25539  dyadss  25545  dyaddisjlem  25546  dyadmax  25549  opnmbllem  25552  itg1addlem2  25648  itg2seq  25693  bddmulibl  25790  limcfval  25823  ellimc3  25830  limciun  25845  dveflem  25933  rolle  25944  dvlip2  25950  c1liplem1  25951  dvgt0lem1  25957  dvgt0  25959  dvlt0  25960  dvne0  25966  dvcnvre  25974  dvfsumrlimge0  25987  ftc1lem6  25998  itgsubst  26006  mdegmullem  26033  ply1domn  26079  fta1g  26125  fta1b  26127  dgrlem  26184  coeid  26193  plydivalg  26257  aannenlem1  26286  aalioulem6  26295  ulmcn  26358  mtestbdd  26364  abelthlem8  26399  efif1olem4  26504  chordthm  26797  xrlimcnp  26928  lgamgulmlem5  26993  isppw2  27075  fsumvma2  27175  perfectlem2  27191  lgsdilem  27285  lgsquad2lem2  27346  lgsquad3  27348  2sqlem5  27383  2sqlem9  27388  rpvmasumlem  27448  dchrisum0flb  27471  pntpbnd  27549  pntibndlem3  27553  pntlem3  27570  pntleml  27572  nosupbday  27667  noinfbday  27682  noetasuplem4  27698  noetainflem4  27702  noetalem1  27703  slerec  27781  madebdaylemlrcut  27854  remulscllem2  28350  tgjustc1  28400  tgjustc2  28401  tgbtwnconn1lem3  28499  legtrid  28516  tglinethru  28561  tglnpt2  28566  tglineintmo  28567  mirreu3  28579  perpcom  28638  footexALT  28643  footex  28646  mideu  28663  opphllem1  28672  lnopp2hpgb  28688  axsegcon  28852  axpasch  28866  axeuclidlem  28887  ecgrtg  28908  elntg  28909  eengtrkg  28911  upgr1eopALT  29042  usgredg4  29142  usgr1eop  29175  usgr1v  29181  subuhgr  29211  subumgr  29213  subusgr  29214  nbuhgr2vtx1edgb  29277  wwlksnext  29821  usgr2wspthon  29893  clwlkclwwlkf1  29937  clwwisshclwwslem  29941  n4cyclfrgr  30218  dlwwlknondlwlknonf1o  30292  vacn  30621  ubthlem1  30797  ubthlem3  30799  minvecolem7  30810  chocunii  31228  pjhthmo  31229  pjhthlem2  31319  nmopub2tALT  31836  nmfnleub2  31853  kbass5  32047  mdslmd1lem1  32252  mdslmd1lem2  32253  mdsymlem5  32334  fcobij  32645  xrofsup  32690  mgcf1o  32929  xrge0tsmsd  33002  symgcntz  33042  archiabllem2a  33138  gsumvsca1  33169  gsumvsca2  33170  isarchiofld  33285  prmidl2  33402  ssmxidl  33435  constrelextdg2  33727  smatrcl  33773  reff  33816  ordtconnlem1  33901  qqhval2  33959  esumpcvgval  34055  imambfm  34240  ballotlemsf1o  34492  signstfvneq0  34550  pconnconn  35199  connpconn  35203  cvmliftmo  35252  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  mrsubff1  35482  msubff1  35524  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  ellines  36116  weiunso  36430  weiunfr  36431  unblimceq0lem  36470  unbdqndv2  36475  irrdiff  37290  matunitlindflem1  37586  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  heicant  37625  opnmbllem0  37626  mblfinlem3  37629  itg2addnclem  37641  itg2addnc  37644  ftc1cnnc  37662  sstotbnd  37745  cntotbnd  37766  ismtyima  37773  heibor1lem  37779  heiborlem10  37790  bfp  37794  rrncmslem  37802  islshpsm  38944  lsatcmp  38967  islshpat  38981  lfl0f  39033  iscvlat2N  39288  ishlat3N  39318  3dim1  39432  islvol5  39544  lvoli2  39546  lncvrelatN  39746  lncmp  39748  paddasslem10  39794  pclfinclN  39915  pexmidlem8N  39942  idltrn  40115  cdleme42keg  40451  cdleme42mgN  40453  cdlemf2  40527  cdlemg2cex  40556  trlcoat  40688  tendoex  40940  erngdvlem4  40956  erngdvlem4-rN  40964  dialss  41011  dibglbN  41131  diblss  41135  dihlsscpre  41199  dihglblem2aN  41258  dihglblem4  41262  dihglblem5  41263  dih1dimatlem  41294  dihglblem6  41305  lcfl7N  41466  lcfrlem9  41515  mapdh9a  41754  hdmapglem7  41894  aks4d1p8  42046  isprimroot  42052  evl1gprodd  42076  hashnexinjle  42088  deg1gprod  42099  sticksstones22  42127  grpods  42153  renegeulemv  42358  sn-subeu  42416  remulinvcom  42422  sn-itrere  42458  sn-retire  42459  imacrhmcl  42484  fidomncyc  42505  fsuppind  42560  prjspertr  42575  prjspreln0  42579  flt4lem7  42629  nna4b4nsq  42630  isnacs3  42680  nacsfix  42682  mzpsubst  42718  eldioph2lem2  42731  eldioph2  42732  eldioph2b  42733  diophin  42742  diophun  42743  rencldnfilem  42790  irrapxlem3  42794  irrapxlem5  42796  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1qrge1  42840  pell1qrgaplem  42843  monotuz  42912  monotoddzzfi  42913  acongtr  42949  acongrep  42951  jm2.26a  42971  jm2.26lem3  42972  jm2.26  42973  jm2.27b  42977  jm2.27  42979  wepwsolem  43013  fnwe2lem2  43022  hbtlem5  43099  hbt  43101  mpaaeu  43121  cantnftermord  43291  cantnfresb  43295  omabs2  43303  tfsconcatun  43308  tfsconcatfn  43309  tfsconcatfv1  43310  tfsconcatfv2  43311  tfsconcatfv  43312  tfsconcatrn  43313  naddcnff  43333  oaun3lem1  43345  rfovcnvf1od  43975  mnurndlem1  44253  fnchoice  45001  rfcnnnub  45008  disjxp1  45041  ioondisj2  45470  iccintsng  45500  fprodcn  45577  lptioo2  45608  lptioo1  45609  limclner  45628  dvdsn1add  45916  stoweidlem14  45991  stoweidlem27  46004  stoweidlem34  46011  stoweidlem49  46026  stoweidlem56  46033  fourierdlem87  46170  iundjiun  46437  ismeannd  46444  hoidmvle  46577  prproropf1olem2  47466  perfectALTVlem2  47684  mogoldbb  47747  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  grimgrtri  47909  isubgr3stgrlem6  47931  rngcinvALTV  48199  ringcinvALTV  48233  lindslinindsimp2lem5  48386  itscnhlinecirc02p  48713  toslat  48904  iinfssclem3  48971  iinfssc  48972  iinfsubc  48973  discsubc  48979  iinfconstbas  48981  imasubc3  49044  upciclem4  49052  tposcurf1  49158  fucofvalg  49177  fuco22  49198  fuco22natlem  49204  functhinclem4  49281  functhincfun  49283  arweuthinc  49362  lanfval  49438  ranfval  49439  islmd  49483  iscmd  49484