Theorem simplrl 800

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  disjxiun  4649  disjxiunOLD  4650  f1imass  6521  f1prex  6539  soisoi  6578  riota5f  6636  tfrlem9a  7482  oeeui  7682  oaabs2  7725  omabs  7727  omxpenlem  8061  fopwdom  8068  frfi  8205  marypha1lem  8339  ordiso2  8420  oismo  8445  wemaplem3  8453  cantnf  8590  isinffi  8818  dfac12lem2  8966  dfac12lem3  8967  infxp  9037  infmap2  9040  infpssrlem5  9129  fin23lem11  9139  fin23lem24  9144  fin23lem26  9147  isf32lem2  9176  isf32lem4  9178  fin1a2lem13  9234  fin1a2s  9236  ttukeylem5  9335  fpwwe2lem12  9463  fpwwe2lem13  9464  wunex2  9560  tskord  9602  prlem934  9855  mulcmpblnr  9892  dedekind  10200  addid1  10216  cnegex  10217  negeu  10271  add20  10540  divdivdiv  10726  ltmul12a  10879  lediv12a  10916  cru  11012  uzwo3  11783  xleadd1a  12083  xlemul1a  12118  ixxun  12191  ixxss12  12195  elfz0ubfz0  12443  mulexpz  12900  leexp1a  12919  expmulnbnd  12996  swrdccat3  13492  abs3lem  14078  rexanre  14086  cau3lem  14094  lo1bdd2  14255  o1lo1  14268  rlimclim1  14276  rlimclim  14277  lo1resb  14295  o1resb  14297  rlimcn2  14321  o1of2  14343  o1rlimmul  14349  lo1add  14357  lo1mul  14358  isercolllem1  14395  climcau  14401  summolem2  14447  summo  14448  o1fsum  14545  prodmolem2  14665  qredeu  15372  isprm5  15419  pclem  15543  pcqmul  15558  pcexp  15564  pcneg  15578  pcprmpw2  15586  pcadd  15593  prmpwdvds  15608  4sqlem13  15661  vdwlem2  15686  vdwlem7  15691  vdwlem11  15695  vdwlem12  15696  ramval  15712  ramz2  15728  ramcl  15733  prmgaplem6  15760  cshwshashlem2  15803  imasval  16171  imasdsval  16175  mreexexd  16308  mreexexdOLD  16309  issubc3  16509  idfucl  16541  funcres2c  16561  fucpropd  16637  xpcval  16817  prfval  16839  evlfcl  16862  curf12  16867  curf1cl  16868  curf2  16869  curfcl  16872  curfuncf  16878  curf2ndf  16887  hof2val  16896  hofcl  16899  hofpropd  16907  yonedalem4a  16915  yonedainv  16921  poslubmo  17146  posglbmo  17147  isipodrs  17161  acsmapd  17178  acsinfd  17180  ismndd  17313  mndpropd  17316  mhmeql  17364  mrcmndind  17366  frmdup3lem  17403  mhmmnd  17537  issubg4  17613  ssnmz  17636  f1otrspeq  17867  psgneu  17926  sylow2blem3  18037  lsmdisj2  18095  pj1eu  18109  efgredlem  18160  frgpuplem  18185  frgpnabl  18278  dmdprdsplitlem  18436  pgpfac1lem3  18476  pgpfaclem3  18482  ringpropd  18582  dvdsrtr  18652  islmhm2  19038  lmhmpropd  19073  assapropd  19327  evlslem1  19515  coe1tmmul2  19646  prmirredlem  19841  psgndiflemA  19947  lsmcss  20036  dsmmlss  20088  uvcf1  20131  frlmup1  20137  mamucl  20207  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  mamulid  20247  mamurid  20248  dmatsubcl  20304  dmatmulcl  20306  mdetunilem7  20424  mdetunilem9  20426  cramer0  20496  cpmatmcllem  20523  mat2pmatf1  20534  decpmatmul  20577  pmatcollpw1  20581  pm2mpf1lem  20599  pm2mpmhmlem2  20624  chpidmat  20652  cpmadugsumlemB  20679  cpmadugsumlemC  20680  toponmre  20897  restbas  20962  iscncl  21073  cnpdis  21097  lmcnp  21108  dishaus  21186  cmpcovf  21194  hauscmplem  21209  dfconn2  21222  clsconn  21233  2ndcctbss  21258  1stccnp  21265  islly2  21287  llyidm  21291  cldllycmp  21298  locfincmp  21329  kgentopon  21341  1stckgenlem  21356  ptpjpre1  21374  ptbasfi  21384  txcls  21407  ptpjopn  21415  xkoccn  21422  txcnp  21423  txcmpb  21447  xkoptsub  21457  xkoco2cn  21461  xkoinjcn  21490  qtopcn  21517  qtoprest  21520  regr1lem  21542  regr1lem2  21543  kqreglem1  21544  qtophmeo  21620  fgabs  21683  hauspwpwf1  21791  flimfnfcls  21832  fclscmp  21834  cnpfcf  21845  ptcmplem4  21859  ptcmplem5  21860  cnextfval  21866  cnextfun  21868  tmdgsum2  21900  tsmsval2  21933  utoptop  22038  utop3cls  22055  ismet2  22138  blin  22226  metss2lem  22316  methaus  22325  met1stc  22326  met2ndci  22327  metcnp  22346  metcnpi3  22351  metustto  22358  metustfbas  22362  nlmvscn  22491  nrginvrcn  22496  nghmcn  22549  xrsxmet  22612  reconnlem1  22629  reconn  22631  xrge0tsms  22637  xmetdcn2  22640  metdscn  22659  addcnlem  22667  mulc1cncf  22708  cncfco  22710  cnheiborlem  22753  cnheibor  22754  nmoleub2lem2  22916  ipcn  23045  iscfil3  23071  cfilfcls  23072  iscmet3  23091  caubl  23106  bcthlem5  23125  rrxdstprj1  23192  minveclem3b  23199  minveclem7  23206  pmltpc  23219  ovolshftlem1  23277  ovolscalem1  23281  ioombl1  23330  uniioombllem6  23356  dyadss  23362  dyaddisjlem  23363  dyadmax  23366  opnmbllem  23369  itg1addlem2  23464  itg2seq  23509  bddmulibl  23605  limcfval  23636  ellimc3  23643  limciun  23658  dveflem  23742  rolle  23753  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  dvgt0  23767  dvlt0  23768  dvne0  23774  dvcnvre  23782  dvfsumrlimge0  23793  ftc1lem6  23804  itgsubst  23812  mdegmullem  23838  ply1domn  23883  fta1g  23927  fta1b  23929  dgrlem  23985  coeid  23994  plydivalg  24054  aannenlem1  24083  aalioulem6  24092  ulmcn  24153  mtestbdd  24159  abelthlem8  24193  efif1olem4  24291  chordthm  24564  xrlimcnp  24695  lgamgulmlem5  24759  isppw2  24841  fsumvma2  24939  perfectlem2  24955  lgsdilem  25049  lgsquad2lem2  25110  lgsquad3  25112  2sqlem5  25147  2sqlem9  25152  rpvmasumlem  25176  dchrisum0flb  25199  pntpbnd  25277  pntibndlem3  25281  pntlem3  25298  pntleml  25300  tgbtwnconn1lem3  25469  legtrid  25486  tglinethru  25531  tglnpt2  25536  tglineintmo  25537  mirreu3  25549  perpcom  25608  footex  25613  mideu  25630  opphllem1  25639  lnopp2hpgb  25655  axsegcon  25807  axpasch  25821  axeuclidlem  25842  ecgrtg  25863  elntg  25864  eengtrkg  25865  upgr1eopALT  26012  usgredg4  26109  usgr1eop  26142  usgr1v  26148  subuhgr  26178  subumgr  26180  subusgr  26181  nbuhgr2vtx1edgb  26248  wwlksnext  26788  usgr2wspthon  26858  clwwisshclwwslem  26927  n4cyclfrgr  27155  vacn  27549  ubthlem1  27726  ubthlem3  27728  minvecolem7  27739  chocunii  28160  pjhthmo  28161  pjhthlem2  28251  nmopub2tALT  28768  nmfnleub2  28785  kbass5  28979  mdslmd1lem1  29184  mdslmd1lem2  29185  mdsymlem5  29266  fcobij  29500  xrofsup  29533  archiabllem2a  29748  gsumvsca1  29782  gsumvsca2  29783  xrge0tsmsd  29785  isarchiofld  29817  smatrcl  29862  reff  29906  ordtconnlem1  29970  qqhval2  30026  esumpcvgval  30140  imambfm  30324  ballotlemsf1o  30575  signstfvneq0  30649  pconnconn  31213  connpconn  31217  cvmliftmo  31266  cvmlift2lem10  31294  cvmlift2lem12  31296  cvmlift3lem7  31307  mrsubff1  31411  msubff1  31453  noprefixmo  31848  noetalem3  31865  slerec  31923  ifscgr  32151  cgrxfr  32162  btwnconn1lem13  32206  ellines  32259  unblimceq0lem  32497  unbdqndv2  32502  matunitlindflem1  33405  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  heicant  33444  opnmbllem0  33445  mblfinlem3  33448  itg2addnclem  33461  itg2addnc  33464  ftc1cnnc  33484  sstotbnd  33574  cntotbnd  33595  ismtyima  33602  heibor1lem  33608  heiborlem10  33619  bfp  33623  rrncmslem  33631  islshpsm  34267  lsatcmp  34290  islshpat  34304  lfl0f  34356  iscvlat2N  34611  ishlat3N  34641  3dim1  34753  islvol5  34865  lvoli2  34867  lncvrelatN  35067  lncmp  35069  paddasslem10  35115  pclfinclN  35236  pexmidlem8N  35263  idltrn  35436  cdleme42keg  35774  cdleme42mgN  35776  cdlemf2  35850  cdlemg2cex  35879  trlcoat  36011  tendoex  36263  erngdvlem4  36279  erngdvlem4-rN  36287  dialss  36335  dibglbN  36455  diblss  36459  dihlsscpre  36523  dihglblem2aN  36582  dihglblem4  36586  dihglblem5  36587  dih1dimatlem  36618  dihglblem6  36629  lcfl7N  36790  lcfrlem9  36839  mapdh9a  37079  hdmapglem7  37221  isnacs3  37273  nacsfix  37275  mzpsubst  37311  eldioph2lem2  37324  eldioph2  37325  eldioph2b  37326  diophin  37336  diophun  37337  rencldnfilem  37384  irrapxlem3  37388  irrapxlem5  37390  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1qrge1  37434  pell1qrgaplem  37437  monotuz  37506  monotoddzzfi  37507  rpexpmord  37513  acongtr  37545  acongrep  37547  jm2.26a  37567  jm2.26lem3  37568  jm2.26  37569  jm2.27b  37573  jm2.27  37575  wepwsolem  37612  fnwe2lem2  37621  hbtlem5  37698  hbt  37700  mpaaeu  37720  rfovcnvf1od  38298  fnchoice  39188  rfcnnnub  39195  disjxp1  39238  ioondisj2  39714  iccintsng  39749  fprodcn  39832  lptioo2  39863  lptioo1  39864  limclner  39883  dvdsn1add  40154  stoweidlem14  40231  stoweidlem27  40244  stoweidlem34  40251  stoweidlem49  40266  stoweidlem56  40273  fourierdlem87  40410  iundjiun  40677  ismeannd  40684  hoidmvle  40814  pfxccat3  41426  perfectALTVlem2  41631  mogoldbb  41673  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  mgmhmeql  41803  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  mndpsuppss  42152  lindslinindsimp2lem5  42251