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  5140  frpomin  6361  f1imass  7284  f1prex  7304  soisoi  7348  riota5f  7416  frxp3  8176  xpord3pred  8177  tfrlem9a  8426  oeeui  8640  oaabs2  8687  omabs  8689  naddssim  8723  omxpenlem  9113  fopwdom  9120  frfi  9321  marypha1lem  9473  ordiso2  9555  oismo  9580  wemaplem3  9588  cantnf  9733  ttrclss  9760  isinffi  10032  dfac12lem2  10185  dfac12lem3  10186  infxp  10254  infmap2  10257  infpssrlem5  10347  fin23lem11  10357  fin23lem24  10362  fin23lem26  10365  isf32lem2  10394  isf32lem4  10396  fin1a2lem13  10452  fin1a2s  10454  ttukeylem5  10553  fpwwe2lem11  10681  fpwwe2lem12  10682  wunex2  10778  tskord  10820  prlem934  11073  mulcmpblnr  11111  dedekind  11424  addrid  11441  cnegex  11442  negeu  11498  add20  11775  divdivdiv  11968  ltmul12a  12123  lediv12a  12161  cru  12258  uzwo3  12985  xleadd1a  13295  xlemul1a  13330  ixxun  13403  ixxss12  13407  elfz0ubfz0  13672  mulexpz  14143  rpexpmord  14208  leexp1a  14215  expmulnbnd  14274  swrdccatin1  14763  pfxccatin12lem3  14770  pfxccat3  14772  abs3lem  15377  rexanre  15385  cau3lem  15393  lo1bdd2  15560  o1lo1  15573  rlimclim1  15581  rlimclim  15582  lo1resb  15600  o1resb  15602  rlimcn3  15626  o1of2  15649  o1rlimmul  15655  lo1add  15663  lo1mul  15664  isercolllem1  15701  climcau  15707  summolem2  15752  summo  15753  o1fsum  15849  prodmolem2  15971  qredeu  16695  isprm5  16744  pclem  16876  pcqmul  16891  pcexp  16897  pcneg  16912  pcprmpw2  16920  pcadd  16927  prmpwdvds  16942  4sqlem13  16995  vdwlem2  17020  vdwlem7  17025  vdwlem11  17029  vdwlem12  17030  ramval  17046  ramz2  17062  ramcl  17067  prmgaplem6  17094  cshwshashlem2  17134  imasval  17556  imasdsval  17560  mreexexd  17691  issubc3  17894  idfucl  17926  funcres2c  17948  fucpropd  18025  xpcval  18222  prfval  18244  evlfcl  18267  curf12  18272  curf1cl  18273  curf2  18274  curfcl  18277  curfuncf  18283  curf2ndf  18292  hof2val  18301  hofcl  18304  hofpropd  18312  yonedalem4a  18320  yonedainv  18326  poslubmo  18456  posglbmo  18457  isipodrs  18582  acsmapd  18599  acsinfd  18601  mgmhmeql  18729  sgrppropd  18744  ismndd  18769  mndpropd  18772  mndpsuppss  18778  mhmeql  18839  mndind  18841  frmdup3lem  18879  mhmmnd  19082  issubg4  19163  ssnmz  19184  f1otrspeq  19465  psgneu  19524  sylow2blem3  19640  lsmdisj2  19700  pj1eu  19714  efgredlem  19765  frgpuplem  19790  frgpnabl  19893  dmdprdsplitlem  20057  pgpfac1lem3  20097  pgpfaclem3  20103  ablsimpgcygd  20126  rngpropd  20171  ringpropd  20285  dvdsrtr  20368  rngcinv  20637  ringcinv  20671  islmhm2  21037  lmhmpropd  21072  prmirredlem  21483  psgndiflemA  21619  lsmcss  21710  dsmmlss  21764  uvcf1  21812  frlmup1  21818  assapropd  21892  evlslem1  22106  coe1tmmul2  22279  mamucl  22405  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  mamulid  22447  mamurid  22448  dmatsubcl  22504  dmatmulcl  22506  mdetunilem7  22624  mdetunilem9  22626  cramer0  22696  cpmatmcllem  22724  mat2pmatf1  22735  decpmatmul  22778  pmatcollpw1  22782  pm2mpf1lem  22800  pm2mpmhmlem2  22825  chpidmat  22853  cpmadugsumlemB  22880  cpmadugsumlemC  22881  toponmre  23101  restbas  23166  iscncl  23277  cnpdis  23301  lmcnp  23312  dishaus  23390  cmpcovf  23399  hauscmplem  23414  dfconn2  23427  clsconn  23438  2ndcctbss  23463  1stccnp  23470  islly2  23492  llyidm  23496  cldllycmp  23503  locfincmp  23534  kgentopon  23546  1stckgenlem  23561  ptpjpre1  23579  ptbasfi  23589  txcls  23612  ptpjopn  23620  xkoccn  23627  txcnp  23628  txcmpb  23652  xkoptsub  23662  xkoco2cn  23666  xkoinjcn  23695  qtopcn  23722  qtoprest  23725  regr1lem  23747  regr1lem2  23748  kqreglem1  23749  qtophmeo  23825  fgabs  23887  hauspwpwf1  23995  flimfnfcls  24036  fclscmp  24038  cnpfcf  24049  ptcmplem4  24063  ptcmplem5  24064  cnextfval  24070  cnextfun  24072  tmdgsum2  24104  tsmsval2  24138  utoptop  24243  utop3cls  24260  ismet2  24343  blin  24431  metss2lem  24524  methaus  24533  met1stc  24534  met2ndci  24535  metcnp  24554  metcnpi3  24559  metustto  24566  metustfbas  24570  nlmvscn  24708  nrginvrcn  24713  nghmcn  24766  xrsxmet  24831  reconnlem1  24848  reconn  24850  xrge0tsms  24856  xmetdcn2  24859  metdscn  24878  addcnlem  24886  mulc1cncf  24931  cncfco  24933  cnheiborlem  24986  cnheibor  24987  nmoleub2lem2  25149  ipcn  25280  iscfil3  25307  cfilfcls  25308  iscmet3  25327  caubl  25342  bcthlem5  25362  rrxdstprj1  25443  minveclem3b  25462  minveclem7  25469  pmltpc  25485  ovolshftlem1  25544  ovolscalem1  25548  ioombl1  25597  uniioombllem6  25623  dyadss  25629  dyaddisjlem  25630  dyadmax  25633  opnmbllem  25636  itg1addlem2  25732  itg2seq  25777  bddmulibl  25874  limcfval  25907  ellimc3  25914  limciun  25929  dveflem  26017  rolle  26028  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  dvgt0  26043  dvlt0  26044  dvne0  26050  dvcnvre  26058  dvfsumrlimge0  26071  ftc1lem6  26082  itgsubst  26090  mdegmullem  26117  ply1domn  26163  fta1g  26209  fta1b  26211  dgrlem  26268  coeid  26277  plydivalg  26341  aannenlem1  26370  aalioulem6  26379  ulmcn  26442  mtestbdd  26448  abelthlem8  26483  efif1olem4  26587  chordthm  26880  xrlimcnp  27011  lgamgulmlem5  27076  isppw2  27158  fsumvma2  27258  perfectlem2  27274  lgsdilem  27368  lgsquad2lem2  27429  lgsquad3  27431  2sqlem5  27466  2sqlem9  27471  rpvmasumlem  27531  dchrisum0flb  27554  pntpbnd  27632  pntibndlem3  27636  pntlem3  27653  pntleml  27655  nosupbday  27750  noinfbday  27765  noetasuplem4  27781  noetainflem4  27785  noetalem1  27786  slerec  27864  madebdaylemlrcut  27937  remulscllem2  28433  tgjustc1  28483  tgjustc2  28484  tgbtwnconn1lem3  28582  legtrid  28599  tglinethru  28644  tglnpt2  28649  tglineintmo  28650  mirreu3  28662  perpcom  28721  footexALT  28726  footex  28729  mideu  28746  opphllem1  28755  lnopp2hpgb  28771  axsegcon  28942  axpasch  28956  axeuclidlem  28977  ecgrtg  28998  elntg  28999  eengtrkg  29001  upgr1eopALT  29134  usgredg4  29234  usgr1eop  29267  usgr1v  29273  subuhgr  29303  subumgr  29305  subusgr  29306  nbuhgr2vtx1edgb  29369  wwlksnext  29913  usgr2wspthon  29985  clwlkclwwlkf1  30029  clwwisshclwwslem  30033  n4cyclfrgr  30310  dlwwlknondlwlknonf1o  30384  vacn  30713  ubthlem1  30889  ubthlem3  30891  minvecolem7  30902  chocunii  31320  pjhthmo  31321  pjhthlem2  31411  nmopub2tALT  31928  nmfnleub2  31945  kbass5  32139  mdslmd1lem1  32344  mdslmd1lem2  32345  mdsymlem5  32426  fcobij  32733  xrofsup  32771  mgcf1o  32993  xrge0tsmsd  33065  symgcntz  33105  archiabllem2a  33201  gsumvsca1  33232  gsumvsca2  33233  isarchiofld  33347  prmidl2  33469  ssmxidl  33502  constrelextdg2  33788  smatrcl  33795  reff  33838  ordtconnlem1  33923  qqhval2  33983  esumpcvgval  34079  imambfm  34264  ballotlemsf1o  34516  signstfvneq0  34587  pconnconn  35236  connpconn  35240  cvmliftmo  35289  cvmlift2lem10  35317  cvmlift2lem12  35319  cvmlift3lem7  35330  mrsubff1  35519  msubff1  35561  ifscgr  36045  cgrxfr  36056  btwnconn1lem13  36100  ellines  36153  weiunso  36467  weiunfr  36468  unblimceq0lem  36507  unbdqndv2  36512  irrdiff  37327  matunitlindflem1  37623  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  heicant  37662  opnmbllem0  37663  mblfinlem3  37666  itg2addnclem  37678  itg2addnc  37681  ftc1cnnc  37699  sstotbnd  37782  cntotbnd  37803  ismtyima  37810  heibor1lem  37816  heiborlem10  37827  bfp  37831  rrncmslem  37839  islshpsm  38981  lsatcmp  39004  islshpat  39018  lfl0f  39070  iscvlat2N  39325  ishlat3N  39355  3dim1  39469  islvol5  39581  lvoli2  39583  lncvrelatN  39783  lncmp  39785  paddasslem10  39831  pclfinclN  39952  pexmidlem8N  39979  idltrn  40152  cdleme42keg  40488  cdleme42mgN  40490  cdlemf2  40564  cdlemg2cex  40593  trlcoat  40725  tendoex  40977  erngdvlem4  40993  erngdvlem4-rN  41001  dialss  41048  dibglbN  41168  diblss  41172  dihlsscpre  41236  dihglblem2aN  41295  dihglblem4  41299  dihglblem5  41300  dih1dimatlem  41331  dihglblem6  41342  lcfl7N  41503  lcfrlem9  41552  mapdh9a  41791  hdmapglem7  41931  aks4d1p8  42088  isprimroot  42094  evl1gprodd  42118  hashnexinjle  42130  deg1gprod  42141  sticksstones22  42169  grpods  42195  renegeulemv  42398  sn-subeu  42456  remulinvcom  42462  sn-itrere  42498  sn-retire  42499  imacrhmcl  42524  fidomncyc  42545  fsuppind  42600  prjspertr  42615  prjspreln0  42619  flt4lem7  42669  nna4b4nsq  42670  isnacs3  42721  nacsfix  42723  mzpsubst  42759  eldioph2lem2  42772  eldioph2  42773  eldioph2b  42774  diophin  42783  diophun  42784  rencldnfilem  42831  irrapxlem3  42835  irrapxlem5  42837  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1qrge1  42881  pell1qrgaplem  42884  monotuz  42953  monotoddzzfi  42954  acongtr  42990  acongrep  42992  jm2.26a  43012  jm2.26lem3  43013  jm2.26  43014  jm2.27b  43018  jm2.27  43020  wepwsolem  43054  fnwe2lem2  43063  hbtlem5  43140  hbt  43142  mpaaeu  43162  cantnftermord  43333  cantnfresb  43337  omabs2  43345  tfsconcatun  43350  tfsconcatfn  43351  tfsconcatfv1  43352  tfsconcatfv2  43353  tfsconcatfv  43354  tfsconcatrn  43355  naddcnff  43375  oaun3lem1  43387  rfovcnvf1od  44017  mnurndlem1  44300  fnchoice  45034  rfcnnnub  45041  disjxp1  45074  ioondisj2  45506  iccintsng  45536  fprodcn  45615  lptioo2  45646  lptioo1  45647  limclner  45666  dvdsn1add  45954  stoweidlem14  46029  stoweidlem27  46042  stoweidlem34  46049  stoweidlem49  46064  stoweidlem56  46071  fourierdlem87  46208  iundjiun  46475  ismeannd  46482  hoidmvle  46615  prproropf1olem2  47491  perfectALTVlem2  47709  mogoldbb  47772  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  grimgrtri  47916  isubgr3stgrlem6  47938  rngcinvALTV  48192  ringcinvALTV  48226  lindslinindsimp2lem5  48379  itscnhlinecirc02p  48706  toslat  48871  upciclem4  48926  tposcurf1  48999  fucofvalg  49013  fuco22  49034  fuco22natlem  49040  functhinclem4  49096  functhincfun  49098