Theorem simplrl 789

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5099  frpomin  6343  f1imass  7268  f1prex  7292  soisoi  7336  riota5f  7405  fnwe2lem3  8149  frxp3  8170  xpord3pred  8171  tfrlem9a  8397  oeeui  8614  oaabs2  8661  omabs  8663  naddssim  8698  omxpenlem  9100  fopwdom  9107  frfi  9279  marypha1lem  9428  ordiso2  9512  oismo  9537  wemaplem3  9545  cantnf  9697  ttrclss  9724  isinffi  10076  dfac12lem2  10226  dfac12lem3  10227  infxp  10295  infmap2  10298  infpssrlem5  10388  fin23lem11  10398  fin23lem24  10403  fin23lem26  10406  isf32lem2  10435  isf32lem4  10437  fin1a2lem13  10493  fin1a2s  10495  ttukeylem5  10594  fpwwe2lem11  10729  fpwwe2lem12  10730  wunex2  10826  tskord  10868  prlem934  11121  mulcmpblnr  11159  dedekind  11476  addrid  11493  cnegex  11494  negeu  11550  add20  11831  divdivdiv  12021  ltmul12a  12176  lediv12a  12213  cru  12315  uzwo3  13073  xleadd1a  13386  xlemul1a  13421  ixxun  13495  ixxss12  13499  elfz0ubfz0  13769  mulexpz  14248  rpexpmord  14314  leexp1a  14321  expmulnbnd  14382  swrdccatin1  14878  pfxccatin12lem3  14885  pfxccat3  14887  abs3lem  15511  rexanre  15519  cau3lem  15527  lo1bdd2  15696  o1lo1  15709  rlimclim1  15717  rlimclim  15718  lo1resb  15736  o1resb  15738  rlimcn3  15762  o1of2  15785  o1rlimmul  15791  lo1add  15799  lo1mul  15800  isercolllem1  15837  climcau  15843  summolem2  15887  summo  15888  o1fsum  15985  prodmolem2  16107  qredeu  16838  isprm5  16888  pclem  17021  pcqmul  17036  pcexp  17042  pcneg  17057  pcprmpw2  17065  pcadd  17072  prmpwdvds  17087  4sqlem13  17140  vdwlem2  17165  vdwlem7  17170  vdwlem11  17174  vdwlem12  17175  ramval  17191  ramz2  17207  ramcl  17212  prmgaplem6  17239  cshwshashlem2  17279  imasval  17688  imasdsval  17692  mreexexd  17827  issubc3  18029  idfucl  18061  funcres2c  18083  fucpropd  18160  xpcval  18356  prfval  18378  evlfcl  18401  curf12  18406  curf1cl  18407  curf2  18408  curfcl  18411  curfuncf  18417  curf2ndf  18426  hof2val  18435  hofcl  18438  hofpropd  18446  yonedalem4a  18454  yonedainv  18460  poslubmo  18588  posglbmo  18589  isipodrs  18716  acsmapd  18733  acsinfd  18735  chnpof1  18809  mgmhmeql  18910  sgrppropd  18925  ismndd  18951  mndpropd  18956  mndpsuppss  18964  mhmeql  19027  mndind  19029  frmdup3lem  19067  mhmmnd  19279  issubg4  19361  ssnmz  19381  f1otrspeq  19666  psgneu  19725  sylow2blem3  19841  lsmdisj2  19901  pj1eu  19915  efgredlem  19966  frgpuplem  19991  frgpnabl  20094  dmdprdsplitlem  20258  pgpfac1lem3  20298  pgpfaclem3  20304  ablsimpgcygd  20327  rngpropd  20401  ringpropd  20524  dvdsrtr  20603  rngcinv  20894  ringcinv  20928  islmhm2  21318  lmhmpropd  21353  prmidl2  21627  prmirredlem  21783  psgndiflemA  21912  lsmcss  22003  dsmmlss  22055  uvcf1  22103  frlmup1  22109  assapropd  22184  evlslem1  22396  coe1tmmul2  22600  mamucl  22721  mamuass  22722  mamudi  22723  mamudir  22724  mamuvs1  22725  mamuvs2  22726  mamulid  22761  mamurid  22762  dmatsubcl  22818  dmatmulcl  22820  mdetunilem7  22938  mdetunilem9  22940  matunitlindflem1  22999  cramer0  23013  cpmatmcllem  23041  mat2pmatf1  23052  decpmatmul  23095  pmatcollpw1  23099  pm2mpf1lem  23117  pm2mpmhmlem2  23142  chpidmat  23170  cpmadugsumlemB  23197  cpmadugsumlemC  23198  toponmre  23416  restbas  23481  iscncl  23592  cnpdis  23616  lmcnp  23627  dishaus  23705  cmpcovf  23714  hauscmplem  23729  dfconn2  23742  clsconn  23753  2ndcctbss  23779  1stccnp  23786  islly2  23808  llyidm  23812  cldllycmp  23819  locfincmp  23850  kgentopon  23862  1stckgenlem  23877  ptpjpre1  23895  ptbasfi  23905  txcls  23928  ptpjopn  23936  xkoccn  23943  txcnp  23944  txcmpb  23968  xkoptsub  23978  xkoco2cn  23982  xkoinjcn  24011  qtopcn  24038  qtoprest  24041  regr1lem  24063  regr1lem2  24064  kqreglem1  24065  qtophmeo  24141  fgabs  24203  hauspwpwf1  24311  flimfnfcls  24352  fclscmp  24354  cnpfcf  24365  ptcmplem4  24379  ptcmplem5  24380  cnextfval  24386  cnextfun  24388  tmdgsum2  24420  tsmsval2  24454  utoptop  24558  utop3cls  24575  ismet2  24657  blin  24745  metss2lem  24835  methaus  24844  met1stc  24845  met2ndci  24846  metcnp  24865  metcnpi3  24870  metustto  24877  metustfbas  24881  nlmvscn  25011  nrginvrcn  25016  nghmcn  25069  xrsxmet  25134  reconnlem1  25151  reconn  25153  xrge0tsms  25159  xmetdcn2  25162  metdscn  25181  addcnlem  25189  mulc1cncf  25231  cncfco  25233  cnheiborlem  25280  cnheibor  25281  nmoleub2lem2  25442  ipcn  25572  iscfil3  25599  cfilfcls  25600  iscmet3  25619  caubl  25634  bcthlem5  25654  rrxdstprj1  25735  minveclem3b  25754  minveclem7  25761  pmltpc  25776  ovolshftlem1  25835  ovolscalem1  25839  ioombl1  25888  uniioombllem6  25914  dyadss  25920  dyaddisjlem  25921  dyadmax  25924  opnmbllem  25927  itg1addlem2  26023  itg2seq  26068  bddmulibl  26164  limcfval  26197  ellimc3  26204  limciun  26219  dveflem  26304  rolle  26315  dvlip2  26320  c1liplem1  26321  dvgt0lem1  26327  dvgt0  26329  dvlt0  26330  dvne0  26336  dvcnvre  26344  dvfsumrlimge0  26355  ftc1lem6  26366  itgsubst  26374  mdegmullem  26401  ply1domn  26447  fta1g  26493  fta1b  26495  dgrlem  26553  coeid  26562  plydivalg  26625  aannenlem1  26660  aalioulem6  26669  ulmcn  26731  mtestbdd  26737  abelthlem8  26771  efif1olem4  26878  chordthm  27170  xrlimcnp  27301  lgamgulmlem5  27365  isppw2  27447  fsumvma2  27546  perfectlem2  27562  lgsdilem  27656  lgsquad2lem2  27717  lgsquad3  27719  2sqlem5  27754  2sqlem9  27759  rpvmasumlem  27819  dchrisum0flb  27842  pntpbnd  27920  pntibndlem3  27924  pntlem3  27941  pntleml  27943  flt4lem7  27994  nna4b4nsq  27995  nosupbday  28067  noinfbday  28082  noetasuplem4  28098  noetainflem4  28102  noetalem1  28103  lesrec  28190  madebdaylemlrcut  28290  bdayons  28667  n0fincut  28746  eucliddivs  28767  bdayfinbndlem1  28858  remulscllem2  28892  tgjustc1  28942  tgjustc2  28943  tgbtwnconn1lem3  29042  legtrid  29059  tglinethru  29109  tglineintmo  29115  tglnpt2  29126  mirreu3  29131  perpcom  29193  footexALT  29198  footex  29201  mideu  29219  opphllem1  29228  lnopp2hpgb  29246  axsegcon  29510  axpasch  29524  axeuclidlem  29545  ecgrtg  29566  elntg  29567  eengtrkg  29569  upgr1eopALT  29700  usgredg4  29803  usgr1eop  29836  usgr1v  29842  subuhgr  29872  subumgr  29874  subusgr  29875  nbuhgr2vtx1edgb  29938  wwlksnext  30487  usgr2wspthon  30562  clwlkclwwlkf1  30606  clwwisshclwwslem  30610  n4cyclfrgr  30897  dlwwlknondlwlknonf1o  30971  vacn  31301  ubthlem1  31477  ubthlem3  31479  minvecolem7  31490  chocunii  31908  pjhthmo  31909  pjhthlem2  31999  nmopub2tALT  32516  nmfnleub2  32533  kbass5  32727  mdslmd1lem1  32932  mdslmd1lem2  32933  mdsymlem5  33014  fcobij  33358  xrofsup  33405  mgcf1o  33610  xrge0tsmsd  33680  symgcntz  33692  archiabllem2a  33801  isarchiofld  33806  gsumvsca1  33833  gsumvsca2  33834  ssmxidl  34045  mplvrpmrhm  34225  constrelextdg2  34425  smatrcl  34474  reff  34517  ordtconnlem1  34602  qqhval2  34660  esumpcvgval  34756  imambfm  34940  ballotlemsf1o  35192  signstfvneq0  35247  j0ltalephlem  35946  pconnconn  36082  connpconn  36086  cvmliftmo  36135  cvmlift2lem10  36163  cvmlift2lem12  36165  cvmlift3lem7  36176  mrsubff1  36365  msubff1  36407  ifscgr  36901  cgrxfr  36912  btwnconn1lem13  36956  ellines  37009  nmuladdss  37054  nadddilem4  37064  weiunso  37346  weiunfr  37347  unblimceq0lem  37464  unbdqndv2  37469  irrdiff  38340  qdiff  38341  poimirlem4  38635  poimirlem13  38644  poimirlem14  38645  heicant  38666  opnmbllem0  38667  mblfinlem3  38670  itg2addnclem  38682  itg2addnc  38685  ftc1cnnc  38703  sstotbnd  38802  cntotbnd  38823  ismtyima  38830  heibor1lem  38836  heiborlem10  38847  bfp  38851  rrncmslem  38859  islshpsm  40130  lsatcmp  40153  islshpat  40167  lfl0f  40219  iscvlat2N  40474  ishlat3N  40504  3dim1  40617  islvol5  40729  lvoli2  40731  lncvrelatN  40931  lncmp  40933  paddasslem10  40979  pclfinclN  41100  pexmidlem8N  41127  idltrn  41300  cdleme42keg  41636  cdleme42mgN  41638  cdlemf2  41712  cdlemg2cex  41741  trlcoat  41873  tendoex  42125  erngdvlem4  42141  erngdvlem4-rN  42149  dialss  42196  dibglbN  42316  diblss  42320  dihlsscpre  42384  dihglblem2aN  42443  dihglblem4  42447  dihglblem5  42448  dih1dimatlem  42479  dihglblem6  42490  lcfl7N  42651  lcfrlem9  42700  mapdh9a  42939  hdmapglem7  43079  aks4d1p8  43230  isprimroot  43236  evl1gprodd  43260  hashnexinjle  43272  deg1gprod  43283  sticksstones22  43311  grpods  43337  renegeulemv  43512  sn-subeu  43571  remulinvcom  43577  imacrhmcl  43674  fidomncyc  43692  fsuppind  43711  prjspertr  43726  prjspreln0  43730  isnacs3  43814  nacsfix  43816  mzpsubst  43852  eldioph2lem2  43865  eldioph2  43866  eldioph2b  43867  diophin  43876  diophun  43877  rencldnfilem  43920  irrapxlem3  43924  irrapxlem5  43926  pell1234qrreccl  43954  pell1234qrmulcl  43955  pell1qrge1  43970  pell1qrgaplem  43973  monotuz  44041  monotoddzzfi  44042  acongtr  44078  acongrep  44080  jm2.26a  44100  jm2.26lem3  44101  jm2.26  44102  jm2.27b  44106  jm2.27  44108  wepwsolem  44142  hbtlem5  44223  hbt  44225  mpaaeu  44245  cantnftermord  44415  cantnfresb  44419  omabs2  44427  tfsconcatun  44432  tfsconcatfn  44433  tfsconcatfv1  44434  tfsconcatfv2  44435  tfsconcatfv  44436  tfsconcatrn  44437  naddcnff  44457  oaun3lem1  44469  rfovcnvf1od  45097  mnurndlem1  45358  fnchoice  46139  rfcnnnub  46146  disjxp1  46179  ioondisj2  46598  iccintsng  46628  fprodcn  46705  lptioo2  46736  lptioo1  46737  limclner  46754  dvdsn1add  47042  stoweidlem14  47117  stoweidlem27  47130  stoweidlem34  47137  stoweidlem49  47152  stoweidlem56  47159  fourierdlem87  47296  iundjiun  47563  ismeannd  47570  hoidmvle  47703  prproropf1olem2  48679  nprmmul2  48703  perfectALTVlem2  48913  mogoldbb  48976  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  grimgrtri  49140  isubgr3stgrlem6  49162  rngcinvALTV  49466  ringcinvALTV  49500  lindslinindsimp2lem5  49667  itscnhlinecirc02p  49990  toslat  50189  iinfssclem3  50263  iinfssc  50264  iinfsubc  50265  discsubc  50271  iinfconstbas  50273  imasubc3  50365  upciclem4  50378  natoppf  50444  tposcurf1  50514  fucofvalg  50533  fuco22  50554  fuco22natlem  50560  functhinclem4  50675  functhincfun  50677  arweuthinc  50757  lanfval  50889  ranfval  50890  islmd  50941  iscmd  50942