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  5104  frpomin  6313  f1imass  7239  f1prex  7259  soisoi  7303  riota5f  7372  frxp3  8130  xpord3pred  8131  tfrlem9a  8354  oeeui  8566  oaabs2  8613  omabs  8615  naddssim  8649  omxpenlem  9042  fopwdom  9049  frfi  9232  marypha1lem  9384  ordiso2  9468  oismo  9493  wemaplem3  9501  cantnf  9646  ttrclss  9673  isinffi  9945  dfac12lem2  10098  dfac12lem3  10099  infxp  10167  infmap2  10170  infpssrlem5  10260  fin23lem11  10270  fin23lem24  10275  fin23lem26  10278  isf32lem2  10307  isf32lem4  10309  fin1a2lem13  10365  fin1a2s  10367  ttukeylem5  10466  fpwwe2lem11  10594  fpwwe2lem12  10595  wunex2  10691  tskord  10733  prlem934  10986  mulcmpblnr  11024  dedekind  11337  addrid  11354  cnegex  11355  negeu  11411  add20  11690  divdivdiv  11883  ltmul12a  12038  lediv12a  12076  cru  12178  uzwo3  12902  xleadd1a  13213  xlemul1a  13248  ixxun  13322  ixxss12  13326  elfz0ubfz0  13593  mulexpz  14067  rpexpmord  14133  leexp1a  14140  expmulnbnd  14200  swrdccatin1  14690  pfxccatin12lem3  14697  pfxccat3  14699  abs3lem  15305  rexanre  15313  cau3lem  15321  lo1bdd2  15490  o1lo1  15503  rlimclim1  15511  rlimclim  15512  lo1resb  15530  o1resb  15532  rlimcn3  15556  o1of2  15579  o1rlimmul  15585  lo1add  15593  lo1mul  15594  isercolllem1  15631  climcau  15637  summolem2  15682  summo  15683  o1fsum  15779  prodmolem2  15901  qredeu  16628  isprm5  16677  pclem  16809  pcqmul  16824  pcexp  16830  pcneg  16845  pcprmpw2  16853  pcadd  16860  prmpwdvds  16875  4sqlem13  16928  vdwlem2  16953  vdwlem7  16958  vdwlem11  16962  vdwlem12  16963  ramval  16979  ramz2  16995  ramcl  17000  prmgaplem6  17027  cshwshashlem2  17067  imasval  17474  imasdsval  17478  mreexexd  17609  issubc3  17811  idfucl  17843  funcres2c  17865  fucpropd  17942  xpcval  18138  prfval  18160  evlfcl  18183  curf12  18188  curf1cl  18189  curf2  18190  curfcl  18193  curfuncf  18199  curf2ndf  18208  hof2val  18217  hofcl  18220  hofpropd  18228  yonedalem4a  18236  yonedainv  18242  poslubmo  18370  posglbmo  18371  isipodrs  18496  acsmapd  18513  acsinfd  18515  mgmhmeql  18643  sgrppropd  18658  ismndd  18683  mndpropd  18686  mndpsuppss  18692  mhmeql  18753  mndind  18755  frmdup3lem  18793  mhmmnd  18996  issubg4  19077  ssnmz  19098  f1otrspeq  19377  psgneu  19436  sylow2blem3  19552  lsmdisj2  19612  pj1eu  19626  efgredlem  19677  frgpuplem  19702  frgpnabl  19805  dmdprdsplitlem  19969  pgpfac1lem3  20009  pgpfaclem3  20015  ablsimpgcygd  20038  rngpropd  20083  ringpropd  20197  dvdsrtr  20277  rngcinv  20546  ringcinv  20580  islmhm2  20945  lmhmpropd  20980  prmirredlem  21382  psgndiflemA  21510  lsmcss  21601  dsmmlss  21653  uvcf1  21701  frlmup1  21707  assapropd  21781  evlslem1  21989  coe1tmmul2  22162  mamucl  22288  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  mamulid  22328  mamurid  22329  dmatsubcl  22385  dmatmulcl  22387  mdetunilem7  22505  mdetunilem9  22507  cramer0  22577  cpmatmcllem  22605  mat2pmatf1  22616  decpmatmul  22659  pmatcollpw1  22663  pm2mpf1lem  22681  pm2mpmhmlem2  22706  chpidmat  22734  cpmadugsumlemB  22761  cpmadugsumlemC  22762  toponmre  22980  restbas  23045  iscncl  23156  cnpdis  23180  lmcnp  23191  dishaus  23269  cmpcovf  23278  hauscmplem  23293  dfconn2  23306  clsconn  23317  2ndcctbss  23342  1stccnp  23349  islly2  23371  llyidm  23375  cldllycmp  23382  locfincmp  23413  kgentopon  23425  1stckgenlem  23440  ptpjpre1  23458  ptbasfi  23468  txcls  23491  ptpjopn  23499  xkoccn  23506  txcnp  23507  txcmpb  23531  xkoptsub  23541  xkoco2cn  23545  xkoinjcn  23574  qtopcn  23601  qtoprest  23604  regr1lem  23626  regr1lem2  23627  kqreglem1  23628  qtophmeo  23704  fgabs  23766  hauspwpwf1  23874  flimfnfcls  23915  fclscmp  23917  cnpfcf  23928  ptcmplem4  23942  ptcmplem5  23943  cnextfval  23949  cnextfun  23951  tmdgsum2  23983  tsmsval2  24017  utoptop  24122  utop3cls  24139  ismet2  24221  blin  24309  metss2lem  24399  methaus  24408  met1stc  24409  met2ndci  24410  metcnp  24429  metcnpi3  24434  metustto  24441  metustfbas  24445  nlmvscn  24575  nrginvrcn  24580  nghmcn  24633  xrsxmet  24698  reconnlem1  24715  reconn  24717  xrge0tsms  24723  xmetdcn2  24726  metdscn  24745  addcnlem  24753  mulc1cncf  24798  cncfco  24800  cnheiborlem  24853  cnheibor  24854  nmoleub2lem2  25016  ipcn  25146  iscfil3  25173  cfilfcls  25174  iscmet3  25193  caubl  25208  bcthlem5  25228  rrxdstprj1  25309  minveclem3b  25328  minveclem7  25335  pmltpc  25351  ovolshftlem1  25410  ovolscalem1  25414  ioombl1  25463  uniioombllem6  25489  dyadss  25495  dyaddisjlem  25496  dyadmax  25499  opnmbllem  25502  itg1addlem2  25598  itg2seq  25643  bddmulibl  25740  limcfval  25773  ellimc3  25780  limciun  25795  dveflem  25883  rolle  25894  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  dvgt0  25909  dvlt0  25910  dvne0  25916  dvcnvre  25924  dvfsumrlimge0  25937  ftc1lem6  25948  itgsubst  25956  mdegmullem  25983  ply1domn  26029  fta1g  26075  fta1b  26077  dgrlem  26134  coeid  26143  plydivalg  26207  aannenlem1  26236  aalioulem6  26245  ulmcn  26308  mtestbdd  26314  abelthlem8  26349  efif1olem4  26454  chordthm  26747  xrlimcnp  26878  lgamgulmlem5  26943  isppw2  27025  fsumvma2  27125  perfectlem2  27141  lgsdilem  27235  lgsquad2lem2  27296  lgsquad3  27298  2sqlem5  27333  2sqlem9  27338  rpvmasumlem  27398  dchrisum0flb  27421  pntpbnd  27499  pntibndlem3  27503  pntlem3  27520  pntleml  27522  nosupbday  27617  noinfbday  27632  noetasuplem4  27648  noetainflem4  27652  noetalem1  27653  slerec  27731  madebdaylemlrcut  27810  bdayon  28173  n0sfincut  28246  eucliddivs  28265  remulscllem2  28352  tgjustc1  28402  tgjustc2  28403  tgbtwnconn1lem3  28501  legtrid  28518  tglinethru  28563  tglnpt2  28568  tglineintmo  28569  mirreu3  28581  perpcom  28640  footexALT  28645  footex  28648  mideu  28665  opphllem1  28674  lnopp2hpgb  28690  axsegcon  28854  axpasch  28868  axeuclidlem  28889  ecgrtg  28910  elntg  28911  eengtrkg  28913  upgr1eopALT  29044  usgredg4  29144  usgr1eop  29177  usgr1v  29183  subuhgr  29213  subumgr  29215  subusgr  29216  nbuhgr2vtx1edgb  29279  wwlksnext  29823  usgr2wspthon  29895  clwlkclwwlkf1  29939  clwwisshclwwslem  29943  n4cyclfrgr  30220  dlwwlknondlwlknonf1o  30294  vacn  30623  ubthlem1  30799  ubthlem3  30801  minvecolem7  30812  chocunii  31230  pjhthmo  31231  pjhthlem2  31321  nmopub2tALT  31838  nmfnleub2  31855  kbass5  32049  mdslmd1lem1  32254  mdslmd1lem2  32255  mdsymlem5  32336  fcobij  32645  xrofsup  32690  mgcf1o  32929  xrge0tsmsd  33002  symgcntz  33042  archiabllem2a  33148  gsumvsca1  33179  gsumvsca2  33180  isarchiofld  33295  prmidl2  33412  ssmxidl  33445  constrelextdg2  33737  smatrcl  33786  reff  33829  ordtconnlem1  33914  qqhval2  33972  esumpcvgval  34068  imambfm  34253  ballotlemsf1o  34505  signstfvneq0  34563  pconnconn  35218  connpconn  35222  cvmliftmo  35271  cvmlift2lem10  35299  cvmlift2lem12  35301  cvmlift3lem7  35312  mrsubff1  35501  msubff1  35543  ifscgr  36032  cgrxfr  36043  btwnconn1lem13  36087  ellines  36140  weiunso  36454  weiunfr  36455  unblimceq0lem  36494  unbdqndv2  36499  irrdiff  37314  matunitlindflem1  37610  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  heicant  37649  opnmbllem0  37650  mblfinlem3  37653  itg2addnclem  37665  itg2addnc  37668  ftc1cnnc  37686  sstotbnd  37769  cntotbnd  37790  ismtyima  37797  heibor1lem  37803  heiborlem10  37814  bfp  37818  rrncmslem  37826  islshpsm  38973  lsatcmp  38996  islshpat  39010  lfl0f  39062  iscvlat2N  39317  ishlat3N  39347  3dim1  39461  islvol5  39573  lvoli2  39575  lncvrelatN  39775  lncmp  39777  paddasslem10  39823  pclfinclN  39944  pexmidlem8N  39971  idltrn  40144  cdleme42keg  40480  cdleme42mgN  40482  cdlemf2  40556  cdlemg2cex  40585  trlcoat  40717  tendoex  40969  erngdvlem4  40985  erngdvlem4-rN  40993  dialss  41040  dibglbN  41160  diblss  41164  dihlsscpre  41228  dihglblem2aN  41287  dihglblem4  41291  dihglblem5  41292  dih1dimatlem  41323  dihglblem6  41334  lcfl7N  41495  lcfrlem9  41544  mapdh9a  41783  hdmapglem7  41923  aks4d1p8  42075  isprimroot  42081  evl1gprodd  42105  hashnexinjle  42117  deg1gprod  42128  sticksstones22  42156  grpods  42182  renegeulemv  42356  sn-subeu  42415  remulinvcom  42421  imacrhmcl  42502  fidomncyc  42523  fsuppind  42578  prjspertr  42593  prjspreln0  42597  flt4lem7  42647  nna4b4nsq  42648  isnacs3  42698  nacsfix  42700  mzpsubst  42736  eldioph2lem2  42749  eldioph2  42750  eldioph2b  42751  diophin  42760  diophun  42761  rencldnfilem  42808  irrapxlem3  42812  irrapxlem5  42814  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1qrge1  42858  pell1qrgaplem  42861  monotuz  42930  monotoddzzfi  42931  acongtr  42967  acongrep  42969  jm2.26a  42989  jm2.26lem3  42990  jm2.26  42991  jm2.27b  42995  jm2.27  42997  wepwsolem  43031  fnwe2lem2  43040  hbtlem5  43117  hbt  43119  mpaaeu  43139  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  44270  fnchoice  45023  rfcnnnub  45030  disjxp1  45063  ioondisj2  45491  iccintsng  45521  fprodcn  45598  lptioo2  45629  lptioo1  45630  limclner  45649  dvdsn1add  45937  stoweidlem14  46012  stoweidlem27  46025  stoweidlem34  46032  stoweidlem49  46047  stoweidlem56  46054  fourierdlem87  46191  iundjiun  46458  ismeannd  46465  hoidmvle  46598  prproropf1olem2  47505  perfectALTVlem2  47723  mogoldbb  47786  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  grimgrtri  47948  isubgr3stgrlem6  47970  rngcinvALTV  48264  ringcinvALTV  48298  lindslinindsimp2lem5  48451  itscnhlinecirc02p  48774  toslat  48970  iinfssclem3  49045  iinfssc  49046  iinfsubc  49047  discsubc  49053  iinfconstbas  49055  imasubc3  49145  upciclem4  49158  natoppf  49218  tposcurf1  49288  fucofvalg  49307  fuco22  49328  fuco22natlem  49334  functhinclem4  49436  functhincfun  49438  arweuthinc  49518  lanfval  49602  ranfval  49603  islmd  49654  iscmd  49655