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  5100  frpomin  6336  f1imass  7260  f1prex  7284  soisoi  7328  riota5f  7397  frxp3  8152  xpord3pred  8153  tfrlem9a  8378  oeeui  8595  oaabs2  8642  omabs  8644  naddssim  8679  omxpenlem  9081  fopwdom  9088  frfi  9260  marypha1lem  9409  ordiso2  9493  oismo  9518  wemaplem3  9526  cantnf  9678  ttrclss  9705  isinffi  10054  dfac12lem2  10204  dfac12lem3  10205  infxp  10273  infmap2  10276  infpssrlem5  10366  fin23lem11  10376  fin23lem24  10381  fin23lem26  10384  isf32lem2  10413  isf32lem4  10415  fin1a2lem13  10471  fin1a2s  10473  ttukeylem5  10572  fpwwe2lem11  10707  fpwwe2lem12  10708  wunex2  10804  tskord  10846  prlem934  11099  mulcmpblnr  11137  dedekind  11454  addrid  11471  cnegex  11472  negeu  11528  add20  11809  divdivdiv  11999  ltmul12a  12154  lediv12a  12191  cru  12293  uzwo3  13051  xleadd1a  13364  xlemul1a  13399  ixxun  13473  ixxss12  13477  elfz0ubfz0  13746  mulexpz  14225  rpexpmord  14291  leexp1a  14298  expmulnbnd  14359  swrdccatin1  14854  pfxccatin12lem3  14861  pfxccat3  14863  abs3lem  15486  rexanre  15494  cau3lem  15502  lo1bdd2  15671  o1lo1  15684  rlimclim1  15692  rlimclim  15693  lo1resb  15711  o1resb  15713  rlimcn3  15737  o1of2  15760  o1rlimmul  15766  lo1add  15774  lo1mul  15775  isercolllem1  15812  climcau  15818  summolem2  15862  summo  15863  o1fsum  15960  prodmolem2  16082  qredeu  16813  isprm5  16863  pclem  16996  pcqmul  17011  pcexp  17017  pcneg  17032  pcprmpw2  17040  pcadd  17047  prmpwdvds  17062  4sqlem13  17115  vdwlem2  17140  vdwlem7  17145  vdwlem11  17149  vdwlem12  17150  ramval  17166  ramz2  17182  ramcl  17187  prmgaplem6  17214  cshwshashlem2  17254  imasval  17663  imasdsval  17667  mreexexd  17802  issubc3  18004  idfucl  18036  funcres2c  18058  fucpropd  18135  xpcval  18331  prfval  18353  evlfcl  18376  curf12  18381  curf1cl  18382  curf2  18383  curfcl  18386  curfuncf  18392  curf2ndf  18401  hof2val  18410  hofcl  18413  hofpropd  18421  yonedalem4a  18429  yonedainv  18435  poslubmo  18563  posglbmo  18564  isipodrs  18691  acsmapd  18708  acsinfd  18710  chnpof1  18784  mgmhmeql  18885  sgrppropd  18900  ismndd  18926  mndpropd  18931  mndpsuppss  18939  mhmeql  19002  mndind  19004  frmdup3lem  19042  mhmmnd  19254  issubg4  19336  ssnmz  19356  f1otrspeq  19641  psgneu  19700  sylow2blem3  19816  lsmdisj2  19876  pj1eu  19890  efgredlem  19941  frgpuplem  19966  frgpnabl  20069  dmdprdsplitlem  20233  pgpfac1lem3  20273  pgpfaclem3  20279  ablsimpgcygd  20302  rngpropd  20376  ringpropd  20499  dvdsrtr  20578  rngcinv  20869  ringcinv  20903  islmhm2  21293  lmhmpropd  21328  prmidl2  21602  prmirredlem  21758  psgndiflemA  21887  lsmcss  21978  dsmmlss  22030  uvcf1  22078  frlmup1  22084  assapropd  22159  evlslem1  22371  coe1tmmul2  22575  mamucl  22696  mamuass  22697  mamudi  22698  mamudir  22699  mamuvs1  22700  mamuvs2  22701  mamulid  22736  mamurid  22737  dmatsubcl  22793  dmatmulcl  22795  mdetunilem7  22913  mdetunilem9  22915  matunitlindflem1  22974  cramer0  22988  cpmatmcllem  23016  mat2pmatf1  23027  decpmatmul  23070  pmatcollpw1  23074  pm2mpf1lem  23092  pm2mpmhmlem2  23117  chpidmat  23145  cpmadugsumlemB  23172  cpmadugsumlemC  23173  toponmre  23391  restbas  23456  iscncl  23567  cnpdis  23591  lmcnp  23602  dishaus  23680  cmpcovf  23689  hauscmplem  23704  dfconn2  23717  clsconn  23728  2ndcctbss  23754  1stccnp  23761  islly2  23783  llyidm  23787  cldllycmp  23794  locfincmp  23825  kgentopon  23837  1stckgenlem  23852  ptpjpre1  23870  ptbasfi  23880  txcls  23903  ptpjopn  23911  xkoccn  23918  txcnp  23919  txcmpb  23943  xkoptsub  23953  xkoco2cn  23957  xkoinjcn  23986  qtopcn  24013  qtoprest  24016  regr1lem  24038  regr1lem2  24039  kqreglem1  24040  qtophmeo  24116  fgabs  24178  hauspwpwf1  24286  flimfnfcls  24327  fclscmp  24329  cnpfcf  24340  ptcmplem4  24354  ptcmplem5  24355  cnextfval  24361  cnextfun  24363  tmdgsum2  24395  tsmsval2  24429  utoptop  24533  utop3cls  24550  ismet2  24632  blin  24720  metss2lem  24810  methaus  24819  met1stc  24820  met2ndci  24821  metcnp  24840  metcnpi3  24845  metustto  24852  metustfbas  24856  nlmvscn  24986  nrginvrcn  24991  nghmcn  25044  xrsxmet  25109  reconnlem1  25126  reconn  25128  xrge0tsms  25134  xmetdcn2  25137  metdscn  25156  addcnlem  25164  mulc1cncf  25206  cncfco  25208  cnheiborlem  25255  cnheibor  25256  nmoleub2lem2  25417  ipcn  25547  iscfil3  25574  cfilfcls  25575  iscmet3  25594  caubl  25609  bcthlem5  25629  rrxdstprj1  25710  minveclem3b  25729  minveclem7  25736  pmltpc  25751  ovolshftlem1  25810  ovolscalem1  25814  ioombl1  25863  uniioombllem6  25889  dyadss  25895  dyaddisjlem  25896  dyadmax  25899  opnmbllem  25902  itg1addlem2  25998  itg2seq  26043  bddmulibl  26139  limcfval  26172  ellimc3  26179  limciun  26194  dveflem  26279  rolle  26290  dvlip2  26295  c1liplem1  26296  dvgt0lem1  26302  dvgt0  26304  dvlt0  26305  dvne0  26311  dvcnvre  26319  dvfsumrlimge0  26330  ftc1lem6  26341  itgsubst  26349  mdegmullem  26376  ply1domn  26422  fta1g  26468  fta1b  26470  dgrlem  26528  coeid  26537  plydivalg  26602  aannenlem1  26637  aalioulem6  26646  ulmcn  26708  mtestbdd  26714  abelthlem8  26748  efif1olem4  26855  chordthm  27147  xrlimcnp  27278  lgamgulmlem5  27342  isppw2  27424  fsumvma2  27523  perfectlem2  27539  lgsdilem  27633  lgsquad2lem2  27694  lgsquad3  27696  2sqlem5  27731  2sqlem9  27736  rpvmasumlem  27796  dchrisum0flb  27819  pntpbnd  27897  pntibndlem3  27901  pntlem3  27918  pntleml  27920  flt4lem7  27971  nna4b4nsq  27972  nosupbday  28044  noinfbday  28059  noetasuplem4  28075  noetainflem4  28079  noetalem1  28080  lesrec  28167  madebdaylemlrcut  28267  bdayons  28644  n0fincut  28723  eucliddivs  28744  bdayfinbndlem1  28835  remulscllem2  28869  tgjustc1  28919  tgjustc2  28920  tgbtwnconn1lem3  29019  legtrid  29036  tglinethru  29086  tglineintmo  29092  tglnpt2  29103  mirreu3  29108  perpcom  29170  footexALT  29175  footex  29178  mideu  29196  opphllem1  29205  lnopp2hpgb  29223  axsegcon  29487  axpasch  29501  axeuclidlem  29522  ecgrtg  29543  elntg  29544  eengtrkg  29546  upgr1eopALT  29677  usgredg4  29780  usgr1eop  29813  usgr1v  29819  subuhgr  29849  subumgr  29851  subusgr  29852  nbuhgr2vtx1edgb  29915  wwlksnext  30464  usgr2wspthon  30539  clwlkclwwlkf1  30583  clwwisshclwwslem  30587  n4cyclfrgr  30874  dlwwlknondlwlknonf1o  30948  vacn  31278  ubthlem1  31454  ubthlem3  31456  minvecolem7  31467  chocunii  31885  pjhthmo  31886  pjhthlem2  31976  nmopub2tALT  32493  nmfnleub2  32510  kbass5  32704  mdslmd1lem1  32909  mdslmd1lem2  32910  mdsymlem5  32991  fcobij  33294  xrofsup  33341  mgcf1o  33546  xrge0tsmsd  33616  symgcntz  33628  archiabllem2a  33737  isarchiofld  33742  gsumvsca1  33769  gsumvsca2  33770  ssmxidl  33981  mplvrpmrhm  34161  constrelextdg2  34361  smatrcl  34410  reff  34453  ordtconnlem1  34538  qqhval2  34596  esumpcvgval  34692  imambfm  34877  ballotlemsf1o  35129  signstfvneq0  35184  pconnconn  35965  connpconn  35969  cvmliftmo  36018  cvmlift2lem10  36046  cvmlift2lem12  36048  cvmlift3lem7  36059  mrsubff1  36248  msubff1  36290  ifscgr  36779  cgrxfr  36790  btwnconn1lem13  36834  ellines  36887  nmuladdss  36932  nadddilem4  36942  weiunso  37224  weiunfr  37225  unblimceq0lem  37342  unbdqndv2  37347  irrdiff  38215  qdiff  38216  poimirlem4  38510  poimirlem13  38519  poimirlem14  38520  heicant  38541  opnmbllem0  38542  mblfinlem3  38545  itg2addnclem  38557  itg2addnc  38560  ftc1cnnc  38578  sstotbnd  38677  cntotbnd  38698  ismtyima  38705  heibor1lem  38711  heiborlem10  38722  bfp  38726  rrncmslem  38734  islshpsm  40005  lsatcmp  40028  islshpat  40042  lfl0f  40094  iscvlat2N  40349  ishlat3N  40379  3dim1  40492  islvol5  40604  lvoli2  40606  lncvrelatN  40806  lncmp  40808  paddasslem10  40854  pclfinclN  40975  pexmidlem8N  41002  idltrn  41175  cdleme42keg  41511  cdleme42mgN  41513  cdlemf2  41587  cdlemg2cex  41616  trlcoat  41748  tendoex  42000  erngdvlem4  42016  erngdvlem4-rN  42024  dialss  42071  dibglbN  42191  diblss  42195  dihlsscpre  42259  dihglblem2aN  42318  dihglblem4  42322  dihglblem5  42323  dih1dimatlem  42354  dihglblem6  42365  lcfl7N  42526  lcfrlem9  42575  mapdh9a  42814  hdmapglem7  42954  aks4d1p8  43105  isprimroot  43111  evl1gprodd  43135  hashnexinjle  43147  deg1gprod  43158  sticksstones22  43186  grpods  43212  renegeulemv  43387  sn-subeu  43446  remulinvcom  43452  imacrhmcl  43546  fidomncyc  43561  fsuppind  43580  prjspertr  43595  prjspreln0  43599  isnacs3  43674  nacsfix  43676  mzpsubst  43712  eldioph2lem2  43725  eldioph2  43726  eldioph2b  43727  diophin  43736  diophun  43737  rencldnfilem  43780  irrapxlem3  43784  irrapxlem5  43786  pell1234qrreccl  43814  pell1234qrmulcl  43815  pell1qrge1  43830  pell1qrgaplem  43833  monotuz  43901  monotoddzzfi  43902  acongtr  43938  acongrep  43940  jm2.26a  43960  jm2.26lem3  43961  jm2.26  43962  jm2.27b  43966  jm2.27  43968  wepwsolem  44002  fnwe2lem2  44011  hbtlem5  44088  hbt  44090  mpaaeu  44110  cantnftermord  44280  cantnfresb  44284  omabs2  44292  tfsconcatun  44297  tfsconcatfn  44298  tfsconcatfv1  44299  tfsconcatfv2  44300  tfsconcatfv  44301  tfsconcatrn  44302  naddcnff  44322  oaun3lem1  44334  rfovcnvf1od  44963  mnurndlem1  45224  fnchoice  45989  rfcnnnub  45996  disjxp1  46029  ioondisj2  46449  iccintsng  46479  fprodcn  46556  lptioo2  46587  lptioo1  46588  limclner  46605  dvdsn1add  46893  stoweidlem14  46968  stoweidlem27  46981  stoweidlem34  46988  stoweidlem49  47003  stoweidlem56  47010  fourierdlem87  47147  iundjiun  47414  ismeannd  47421  hoidmvle  47554  prproropf1olem2  48530  nprmmul2  48554  perfectALTVlem2  48764  mogoldbb  48827  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  grimgrtri  48991  isubgr3stgrlem6  49013  rngcinvALTV  49317  ringcinvALTV  49351  lindslinindsimp2lem5  49518  itscnhlinecirc02p  49841  toslat  50034  iinfssclem3  50108  iinfssc  50109  iinfsubc  50110  discsubc  50116  iinfconstbas  50118  imasubc3  50208  upciclem4  50221  natoppf  50281  tposcurf1  50351  fucofvalg  50370  fuco22  50391  fuco22natlem  50397  functhinclem4  50499  functhincfun  50501  arweuthinc  50581  lanfval  50665  ranfval  50666  islmd  50717  iscmd  50718