Theorem simplrl 773

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  disjxiun  5144  frpomin  6340  f1imass  7265  f1prex  7284  soisoi  7327  riota5f  7396  frxp3  8139  xpord3pred  8140  tfrlem9a  8388  oeeui  8604  oaabs2  8650  omabs  8652  naddssim  8686  omxpenlem  9075  fopwdom  9082  frfi  9290  marypha1lem  9430  ordiso2  9512  oismo  9537  wemaplem3  9545  cantnf  9690  ttrclss  9717  isinffi  9989  dfac12lem2  10141  dfac12lem3  10142  infxp  10212  infmap2  10215  infpssrlem5  10304  fin23lem11  10314  fin23lem24  10319  fin23lem26  10322  isf32lem2  10351  isf32lem4  10353  fin1a2lem13  10409  fin1a2s  10411  ttukeylem5  10510  fpwwe2lem11  10638  fpwwe2lem12  10639  wunex2  10735  tskord  10777  prlem934  11030  mulcmpblnr  11068  dedekind  11381  addrid  11398  cnegex  11399  negeu  11454  add20  11730  divdivdiv  11919  ltmul12a  12074  lediv12a  12111  cru  12208  uzwo3  12931  xleadd1a  13236  xlemul1a  13271  ixxun  13344  ixxss12  13348  elfz0ubfz0  13609  mulexpz  14072  rpexpmord  14137  leexp1a  14144  expmulnbnd  14202  swrdccatin1  14679  pfxccatin12lem3  14686  pfxccat3  14688  abs3lem  15289  rexanre  15297  cau3lem  15305  lo1bdd2  15472  o1lo1  15485  rlimclim1  15493  rlimclim  15494  lo1resb  15512  o1resb  15514  rlimcn3  15538  o1of2  15561  o1rlimmul  15567  lo1add  15575  lo1mul  15576  isercolllem1  15615  climcau  15621  summolem2  15666  summo  15667  o1fsum  15763  prodmolem2  15883  qredeu  16599  isprm5  16648  pclem  16775  pcqmul  16790  pcexp  16796  pcneg  16811  pcprmpw2  16819  pcadd  16826  prmpwdvds  16841  4sqlem13  16894  vdwlem2  16919  vdwlem7  16924  vdwlem11  16928  vdwlem12  16929  ramval  16945  ramz2  16961  ramcl  16966  prmgaplem6  16993  cshwshashlem2  17034  imasval  17461  imasdsval  17465  mreexexd  17596  issubc3  17803  idfucl  17835  funcres2c  17856  fucpropd  17934  xpcval  18133  prfval  18155  evlfcl  18179  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  curfuncf  18195  curf2ndf  18204  hof2val  18213  hofcl  18216  hofpropd  18224  yonedalem4a  18232  yonedainv  18238  poslubmo  18368  posglbmo  18369  isipodrs  18494  acsmapd  18511  acsinfd  18513  mgmhmeql  18641  sgrppropd  18656  ismndd  18681  mndpropd  18684  mhmeql  18743  mndind  18745  frmdup3lem  18783  mhmmnd  18983  issubg4  19061  ssnmz  19082  f1otrspeq  19356  psgneu  19415  sylow2blem3  19531  lsmdisj2  19591  pj1eu  19605  efgredlem  19656  frgpuplem  19681  frgpnabl  19784  dmdprdsplitlem  19948  pgpfac1lem3  19988  pgpfaclem3  19994  ablsimpgcygd  20017  rngpropd  20068  ringpropd  20176  dvdsrtr  20259  islmhm2  20793  lmhmpropd  20828  prmirredlem  21243  psgndiflemA  21373  lsmcss  21464  dsmmlss  21518  uvcf1  21566  frlmup1  21572  assapropd  21645  evlslem1  21864  coe1tmmul2  22018  mamucl  22121  mamuass  22122  mamudi  22123  mamudir  22124  mamuvs1  22125  mamuvs2  22126  mamulid  22163  mamurid  22164  dmatsubcl  22220  dmatmulcl  22222  mdetunilem7  22340  mdetunilem9  22342  cramer0  22412  cpmatmcllem  22440  mat2pmatf1  22451  decpmatmul  22494  pmatcollpw1  22498  pm2mpf1lem  22516  pm2mpmhmlem2  22541  chpidmat  22569  cpmadugsumlemB  22596  cpmadugsumlemC  22597  toponmre  22817  restbas  22882  iscncl  22993  cnpdis  23017  lmcnp  23028  dishaus  23106  cmpcovf  23115  hauscmplem  23130  dfconn2  23143  clsconn  23154  2ndcctbss  23179  1stccnp  23186  islly2  23208  llyidm  23212  cldllycmp  23219  locfincmp  23250  kgentopon  23262  1stckgenlem  23277  ptpjpre1  23295  ptbasfi  23305  txcls  23328  ptpjopn  23336  xkoccn  23343  txcnp  23344  txcmpb  23368  xkoptsub  23378  xkoco2cn  23382  xkoinjcn  23411  qtopcn  23438  qtoprest  23441  regr1lem  23463  regr1lem2  23464  kqreglem1  23465  qtophmeo  23541  fgabs  23603  hauspwpwf1  23711  flimfnfcls  23752  fclscmp  23754  cnpfcf  23765  ptcmplem4  23779  ptcmplem5  23780  cnextfval  23786  cnextfun  23788  tmdgsum2  23820  tsmsval2  23854  utoptop  23959  utop3cls  23976  ismet2  24059  blin  24147  metss2lem  24240  methaus  24249  met1stc  24250  met2ndci  24251  metcnp  24270  metcnpi3  24275  metustto  24282  metustfbas  24286  nlmvscn  24424  nrginvrcn  24429  nghmcn  24482  xrsxmet  24545  reconnlem1  24562  reconn  24564  xrge0tsms  24570  xmetdcn2  24573  metdscn  24592  addcnlem  24600  mulc1cncf  24645  cncfco  24647  cnheiborlem  24700  cnheibor  24701  nmoleub2lem2  24863  ipcn  24994  iscfil3  25021  cfilfcls  25022  iscmet3  25041  caubl  25056  bcthlem5  25076  rrxdstprj1  25157  minveclem3b  25176  minveclem7  25183  pmltpc  25199  ovolshftlem1  25258  ovolscalem1  25262  ioombl1  25311  uniioombllem6  25337  dyadss  25343  dyaddisjlem  25344  dyadmax  25347  opnmbllem  25350  itg1addlem2  25446  itg2seq  25492  bddmulibl  25588  limcfval  25621  ellimc3  25628  limciun  25643  dveflem  25731  rolle  25742  dvlip2  25747  c1liplem1  25748  dvgt0lem1  25754  dvgt0  25756  dvlt0  25757  dvne0  25763  dvcnvre  25771  dvfsumrlimge0  25782  ftc1lem6  25793  itgsubst  25801  mdegmullem  25831  ply1domn  25876  fta1g  25920  fta1b  25922  dgrlem  25978  coeid  25987  plydivalg  26048  aannenlem1  26077  aalioulem6  26086  ulmcn  26147  mtestbdd  26153  abelthlem8  26187  efif1olem4  26290  chordthm  26578  xrlimcnp  26709  lgamgulmlem5  26773  isppw2  26855  fsumvma2  26953  perfectlem2  26969  lgsdilem  27063  lgsquad2lem2  27124  lgsquad3  27126  2sqlem5  27161  2sqlem9  27166  rpvmasumlem  27226  dchrisum0flb  27249  pntpbnd  27327  pntibndlem3  27331  pntlem3  27348  pntleml  27350  nosupbday  27444  noinfbday  27459  noetasuplem4  27475  noetainflem4  27479  noetalem1  27480  slerec  27557  madebdaylemlrcut  27630  tgjustc1  27993  tgjustc2  27994  tgbtwnconn1lem3  28092  legtrid  28109  tglinethru  28154  tglnpt2  28159  tglineintmo  28160  mirreu3  28172  perpcom  28231  footexALT  28236  footex  28239  mideu  28256  opphllem1  28265  lnopp2hpgb  28281  axsegcon  28452  axpasch  28466  axeuclidlem  28487  ecgrtg  28508  elntg  28509  eengtrkg  28511  upgr1eopALT  28644  usgredg4  28741  usgr1eop  28774  usgr1v  28780  subuhgr  28810  subumgr  28812  subusgr  28813  nbuhgr2vtx1edgb  28876  wwlksnext  29414  usgr2wspthon  29486  clwlkclwwlkf1  29530  clwwisshclwwslem  29534  n4cyclfrgr  29811  dlwwlknondlwlknonf1o  29885  vacn  30214  ubthlem1  30390  ubthlem3  30392  minvecolem7  30403  chocunii  30821  pjhthmo  30822  pjhthlem2  30912  nmopub2tALT  31429  nmfnleub2  31446  kbass5  31640  mdslmd1lem1  31845  mdslmd1lem2  31846  mdsymlem5  31927  fcobij  32214  xrofsup  32247  mgcf1o  32440  xrge0tsmsd  32479  symgcntz  32516  archiabllem2a  32610  gsumvsca1  32641  gsumvsca2  32642  isarchiofld  32705  prmidl2  32833  ssmxidl  32864  smatrcl  33074  reff  33117  ordtconnlem1  33202  qqhval2  33260  esumpcvgval  33374  imambfm  33559  ballotlemsf1o  33810  signstfvneq0  33881  pconnconn  34520  connpconn  34524  cvmliftmo  34573  cvmlift2lem10  34601  cvmlift2lem12  34603  cvmlift3lem7  34614  mrsubff1  34803  msubff1  34845  ifscgr  35320  cgrxfr  35331  btwnconn1lem13  35375  ellines  35428  unblimceq0lem  35685  unbdqndv2  35690  irrdiff  36510  matunitlindflem1  36787  poimirlem4  36795  poimirlem13  36804  poimirlem14  36805  heicant  36826  opnmbllem0  36827  mblfinlem3  36830  itg2addnclem  36842  itg2addnc  36845  ftc1cnnc  36863  sstotbnd  36946  cntotbnd  36967  ismtyima  36974  heibor1lem  36980  heiborlem10  36991  bfp  36995  rrncmslem  37003  islshpsm  38153  lsatcmp  38176  islshpat  38190  lfl0f  38242  iscvlat2N  38497  ishlat3N  38527  3dim1  38641  islvol5  38753  lvoli2  38755  lncvrelatN  38955  lncmp  38957  paddasslem10  39003  pclfinclN  39124  pexmidlem8N  39151  idltrn  39324  cdleme42keg  39660  cdleme42mgN  39662  cdlemf2  39736  cdlemg2cex  39765  trlcoat  39897  tendoex  40149  erngdvlem4  40165  erngdvlem4-rN  40173  dialss  40220  dibglbN  40340  diblss  40344  dihlsscpre  40408  dihglblem2aN  40467  dihglblem4  40471  dihglblem5  40472  dih1dimatlem  40503  dihglblem6  40514  lcfl7N  40675  lcfrlem9  40724  mapdh9a  40963  hdmapglem7  41103  aks4d1p8  41258  sticksstones22  41290  imacrhmcl  41393  fsuppind  41464  renegeulemv  41543  sn-subeu  41601  remulinvcom  41607  itrere  41641  retire  41642  prjspertr  41649  prjspreln0  41653  flt4lem7  41703  nna4b4nsq  41704  isnacs3  41750  nacsfix  41752  mzpsubst  41788  eldioph2lem2  41801  eldioph2  41802  eldioph2b  41803  diophin  41812  diophun  41813  rencldnfilem  41860  irrapxlem3  41864  irrapxlem5  41866  pell1234qrreccl  41894  pell1234qrmulcl  41895  pell1qrge1  41910  pell1qrgaplem  41913  monotuz  41982  monotoddzzfi  41983  acongtr  42019  acongrep  42021  jm2.26a  42041  jm2.26lem3  42042  jm2.26  42043  jm2.27b  42047  jm2.27  42049  wepwsolem  42086  fnwe2lem2  42095  hbtlem5  42172  hbt  42174  mpaaeu  42194  cantnftermord  42372  cantnfresb  42376  omabs2  42384  tfsconcatun  42389  tfsconcatfn  42390  tfsconcatfv1  42391  tfsconcatfv2  42392  tfsconcatfv  42393  tfsconcatrn  42394  naddcnff  42414  oaun3lem1  42426  rfovcnvf1od  43057  mnurndlem1  43342  fnchoice  44015  rfcnnnub  44022  disjxp1  44057  ioondisj2  44504  iccintsng  44534  fprodcn  44614  lptioo2  44645  lptioo1  44646  limclner  44665  dvdsn1add  44953  stoweidlem14  45028  stoweidlem27  45041  stoweidlem34  45048  stoweidlem49  45063  stoweidlem56  45070  fourierdlem87  45207  iundjiun  45474  ismeannd  45481  hoidmvle  45614  prproropf1olem2  46470  perfectALTVlem2  46688  mogoldbb  46751  bgoldbtbndlem2  46772  bgoldbtbndlem3  46773  rngcinv  46967  rngcinvALTV  46979  ringcinv  47018  ringcinvALTV  47042  mndpsuppss  47135  lindslinindsimp2lem5  47230  itscnhlinecirc02p  47558  toslat  47694  functhinclem4  47751