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  5103  frpomin  6364  f1imass  7294  f1prex  7318  soisoi  7362  riota5f  7431  fnwe2lem3  8177  frxp3  8198  xpord3pred  8199  tfrlem9a  8425  oeeui  8642  oaabs2  8689  omabs  8691  naddssim  8726  omxpenlem  9128  fopwdom  9135  frfi  9307  marypha1lem  9455  ordiso2  9539  oismo  9564  wemaplem3  9572  cantnf  9724  ttrclss  9751  isinffi  10103  dfac12lem2  10253  dfac12lem3  10254  infxp  10322  infmap2  10325  infpssrlem5  10415  fin23lem11  10425  fin23lem24  10430  fin23lem26  10433  isf32lem2  10462  isf32lem4  10464  fin1a2lem13  10520  fin1a2s  10522  ttukeylem5  10621  fpwwe2lem11  10756  fpwwe2lem12  10757  wunex2  10853  tskord  10895  prlem934  11148  mulcmpblnr  11186  dedekind  11503  addrid  11520  cnegex  11521  negeu  11577  add20  11858  divdivdiv  12048  ltmul12a  12203  lediv12a  12240  cru  12342  uzwo3  13100  xleadd1a  13413  xlemul1a  13448  ixxun  13522  ixxss12  13526  elfz0ubfz0  13796  mulexpz  14275  rpexpmord  14341  leexp1a  14348  expmulnbnd  14409  swrdccatin1  14905  pfxccatin12lem3  14912  pfxccat3  14914  abs3lem  15538  rexanre  15546  cau3lem  15554  lo1bdd2  15723  o1lo1  15736  rlimclim1  15744  rlimclim  15745  lo1resb  15763  o1resb  15765  rlimcn3  15789  o1of2  15812  o1rlimmul  15818  lo1add  15826  lo1mul  15827  isercolllem1  15864  climcau  15870  summolem2  15914  summo  15915  o1fsum  16012  prodmolem2  16134  qredeu  16865  isprm5  16915  pclem  17048  pcqmul  17063  pcexp  17069  pcneg  17084  pcprmpw2  17092  pcadd  17099  prmpwdvds  17114  4sqlem13  17167  vdwlem2  17192  vdwlem7  17197  vdwlem11  17201  vdwlem12  17202  ramval  17218  ramz2  17234  ramcl  17239  prmgaplem6  17266  cshwshashlem2  17306  imasval  17715  imasdsval  17719  mreexexd  17854  issubc3  18056  idfucl  18088  funcres2c  18110  fucpropd  18187  xpcval  18383  prfval  18405  evlfcl  18428  curf12  18433  curf1cl  18434  curf2  18435  curfcl  18438  curfuncf  18444  curf2ndf  18453  hof2val  18462  hofcl  18465  hofpropd  18473  yonedalem4a  18481  yonedainv  18487  poslubmo  18615  posglbmo  18616  isipodrs  18743  acsmapd  18760  acsinfd  18762  chnpof1  18836  mgmhmeql  18937  sgrppropd  18952  ismndd  18978  mndpropd  18983  mndpsuppss  18991  mhmeql  19054  mndind  19056  frmdup3lem  19094  mhmmnd  19306  issubg4  19388  ssnmz  19408  f1otrspeq  19694  psgneu  19753  sylow2blem3  19869  lsmdisj2  19929  pj1eu  19943  efgredlem  19994  frgpuplem  20019  frgpnabl  20122  dmdprdsplitlem  20286  pgpfac1lem3  20326  pgpfaclem3  20332  ablsimpgcygd  20355  rngpropd  20429  ringpropd  20552  dvdsrtr  20631  rngcinv  20922  ringcinv  20956  islmhm2  21346  lmhmpropd  21381  prmidl2  21655  prmirredlem  21811  psgndiflemA  21940  lsmcss  22031  dsmmlss  22083  uvcf1  22131  frlmup1  22137  assapropd  22212  evlslem1  22424  coe1tmmul2  22628  mamucl  22749  mamuass  22750  mamudi  22751  mamudir  22752  mamuvs1  22753  mamuvs2  22754  mamulid  22789  mamurid  22790  dmatsubcl  22846  dmatmulcl  22848  mdetunilem7  22966  mdetunilem9  22968  matunitlindflem1  23027  cramer0  23041  cpmatmcllem  23069  mat2pmatf1  23080  decpmatmul  23123  pmatcollpw1  23127  pm2mpf1lem  23145  pm2mpmhmlem2  23170  chpidmat  23198  cpmadugsumlemB  23225  cpmadugsumlemC  23226  toponmre  23444  restbas  23509  iscncl  23620  cnpdis  23644  lmcnp  23655  dishaus  23733  cmpcovf  23742  hauscmplem  23757  dfconn2  23770  clsconn  23781  2ndcctbss  23807  1stccnp  23814  islly2  23836  llyidm  23840  cldllycmp  23847  locfincmp  23878  kgentopon  23890  1stckgenlem  23905  ptpjpre1  23923  ptbasfi  23933  txcls  23956  ptpjopn  23964  xkoccn  23971  txcnp  23972  txcmpb  23996  xkoptsub  24006  xkoco2cn  24010  xkoinjcn  24039  qtopcn  24066  qtoprest  24069  regr1lem  24091  regr1lem2  24092  kqreglem1  24093  qtophmeo  24169  fgabs  24231  hauspwpwf1  24339  flimfnfcls  24380  fclscmp  24382  cnpfcf  24393  ptcmplem4  24407  ptcmplem5  24408  cnextfval  24414  cnextfun  24416  tmdgsum2  24448  tsmsval2  24482  utoptop  24586  utop3cls  24603  ismet2  24685  blin  24773  metss2lem  24863  methaus  24872  met1stc  24873  met2ndci  24874  metcnp  24893  metcnpi3  24898  metustto  24905  metustfbas  24909  nlmvscn  25039  nrginvrcn  25044  nghmcn  25097  xrsxmet  25162  reconnlem1  25179  reconn  25181  xrge0tsms  25187  xmetdcn2  25190  metdscn  25209  addcnlem  25217  mulc1cncf  25259  cncfco  25261  cnheiborlem  25308  cnheibor  25309  nmoleub2lem2  25470  ipcn  25600  iscfil3  25627  cfilfcls  25628  iscmet3  25647  caubl  25662  bcthlem5  25682  rrxdstprj1  25763  minveclem3b  25782  minveclem7  25789  pmltpc  25804  ovolshftlem1  25863  ovolscalem1  25867  ioombl1  25916  uniioombllem6  25942  dyadss  25948  dyaddisjlem  25949  dyadmax  25952  opnmbllem  25955  itg1addlem2  26051  itg2seq  26096  bddmulibl  26192  limcfval  26225  ellimc3  26232  limciun  26247  dveflem  26332  rolle  26343  dvlip2  26348  c1liplem1  26349  dvgt0lem1  26355  dvgt0  26357  dvlt0  26358  dvne0  26364  dvcnvre  26372  dvfsumrlimge0  26383  ftc1lem6  26394  itgsubst  26402  mdegmullem  26429  ply1domn  26475  fta1g  26521  fta1b  26523  dgrlem  26581  coeid  26590  plydivalg  26653  aannenlem1  26688  aalioulem6  26697  ulmcn  26759  mtestbdd  26765  abelthlem8  26799  efif1olem4  26906  chordthm  27198  xrlimcnp  27329  lgamgulmlem5  27393  isppw2  27475  fsumvma2  27574  perfectlem2  27590  lgsdilem  27684  lgsquad2lem2  27745  lgsquad3  27747  2sqlem5  27782  2sqlem9  27787  rpvmasumlem  27847  dchrisum0flb  27870  pntpbnd  27948  pntibndlem3  27952  pntlem3  27969  pntleml  27971  flt4lem7  28022  nna4b4nsq  28023  nosupbday  28095  noinfbday  28110  noetasuplem4  28126  noetainflem4  28130  noetalem1  28131  lesrec  28218  madebdaylemlrcut  28318  bdayons  28695  n0fincut  28774  eucliddivs  28795  bdayfinbndlem1  28886  remulscllem2  28920  tgjustc1  28970  tgjustc2  28971  tgbtwnconn1lem3  29070  legtrid  29087  tglinethru  29137  tglineintmo  29143  tglnpt2  29154  mirreu3  29159  perpcom  29221  footexALT  29226  footex  29229  mideu  29247  opphllem1  29256  lnopp2hpgb  29274  axsegcon  29538  axpasch  29552  axeuclidlem  29573  ecgrtg  29594  elntg  29595  eengtrkg  29597  upgr1eopALT  29728  usgredg4  29831  usgr1eop  29864  usgr1v  29870  subuhgr  29900  subumgr  29902  subusgr  29903  nbuhgr2vtx1edgb  29966  wwlksnext  30515  usgr2wspthon  30590  clwlkclwwlkf1  30634  clwwisshclwwslem  30638  n4cyclfrgr  30925  dlwwlknondlwlknonf1o  30999  vacn  31329  ubthlem1  31505  ubthlem3  31507  minvecolem7  31518  chocunii  31936  pjhthmo  31937  pjhthlem2  32027  nmopub2tALT  32544  nmfnleub2  32561  kbass5  32755  mdslmd1lem1  32960  mdslmd1lem2  32961  mdsymlem5  33042  fcobij  33385  xrofsup  33432  mgcf1o  33640  xrge0tsmsd  33710  symgcntz  33722  archiabllem2a  33831  isarchiofld  33836  gsumvsca1  33863  gsumvsca2  33864  ssmxidl  34083  mplvrpmrhm  34262  constrelextdg2  34462  smatrcl  34511  reff  34554  ordtconnlem1  34639  qqhval2  34697  esumpcvgval  34793  imambfm  34977  ballotlemsf1o  35229  signstfvneq0  35284  j0ltalephlem  36020  pconnconn  36176  connpconn  36180  cvmliftmo  36229  cvmlift2lem10  36257  cvmlift2lem12  36259  cvmlift3lem7  36270  mrsubff1  36459  msubff1  36501  ifscgr  37000  cgrxfr  37011  btwnconn1lem13  37055  ellines  37108  nmuladdss  37153  nadddilem4  37163  weiunso  37445  weiunfr  37446  unblimceq0lem  37563  unbdqndv2  37568  irrdiff  38452  qdiff  38453  poimirlem4  38747  poimirlem13  38756  poimirlem14  38757  heicant  38778  opnmbllem0  38779  mblfinlem3  38782  itg2addnclem  38794  itg2addnc  38797  ftc1cnnc  38815  sstotbnd  38912  cntotbnd  38933  ismtyima  38940  heibor1lem  38946  heiborlem10  38957  bfp  38961  rrncmslem  38969  islshpsm  40240  lsatcmp  40263  islshpat  40277  lfl0f  40329  iscvlat2N  40584  ishlat3N  40614  3dim1  40727  islvol5  40839  lvoli2  40841  lncvrelatN  41041  lncmp  41043  paddasslem10  41089  pclfinclN  41210  pexmidlem8N  41237  idltrn  41410  cdleme42keg  41746  cdleme42mgN  41748  cdlemf2  41822  cdlemg2cex  41851  trlcoat  41983  tendoex  42235  erngdvlem4  42251  erngdvlem4-rN  42259  dialss  42306  dibglbN  42426  diblss  42430  dihlsscpre  42494  dihglblem2aN  42553  dihglblem4  42557  dihglblem5  42558  dih1dimatlem  42589  dihglblem6  42600  lcfl7N  42761  lcfrlem9  42810  mapdh9a  43049  hdmapglem7  43189  aks4d1p8  43340  isprimroot  43346  evl1gprodd  43370  hashnexinjle  43382  deg1gprod  43393  sticksstones22  43421  grpods  43447  renegeulemv  43623  sn-subeu  43682  remulinvcom  43688  imacrhmcl  43785  fidomncyc  43803  fsuppind  43822  prjspertr  43837  prjspreln0  43841  isnacs3  43925  nacsfix  43927  mzpsubst  43963  eldioph2lem2  43976  eldioph2  43977  eldioph2b  43978  diophin  43987  diophun  43988  rencldnfilem  44031  irrapxlem3  44035  irrapxlem5  44037  pell1234qrreccl  44065  pell1234qrmulcl  44066  pell1qrge1  44081  pell1qrgaplem  44084  monotuz  44152  monotoddzzfi  44153  acongtr  44189  acongrep  44191  jm2.26a  44211  jm2.26lem3  44212  jm2.26  44213  jm2.27b  44217  jm2.27  44219  wepwsolem  44253  hbtlem5  44333  hbt  44335  mpaaeu  44355  cantnftermord  44525  cantnfresb  44529  omabs2  44537  tfsconcatun  44542  tfsconcatfn  44543  tfsconcatfv1  44544  tfsconcatfv2  44545  tfsconcatfv  44546  tfsconcatrn  44547  naddcnff  44567  oaun3lem1  44579  rfovcnvf1od  45207  mnurndlem1  45468  fnchoice  46262  rfcnnnub  46269  disjxp1  46302  ioondisj2  46720  iccintsng  46750  fprodcn  46827  lptioo2  46858  lptioo1  46859  limclner  46876  dvdsn1add  47164  stoweidlem14  47239  stoweidlem27  47252  stoweidlem34  47259  stoweidlem49  47274  stoweidlem56  47281  fourierdlem87  47418  iundjiun  47685  ismeannd  47692  hoidmvle  47825  prproropf1olem2  48801  nprmmul2  48825  perfectALTVlem2  49035  mogoldbb  49098  bgoldbtbndlem2  49119  bgoldbtbndlem3  49120  grimgrtri  49262  isubgr3stgrlem6  49284  rngcinvALTV  49588  ringcinvALTV  49622  lindslinindsimp2lem5  49789  itscnhlinecirc02p  50112  toslat  50311  iinfssclem3  50385  iinfssc  50386  iinfsubc  50387  discsubc  50393  iinfconstbas  50395  imasubc3  50487  upciclem4  50500  natoppf  50566  tposcurf1  50636  fucofvalg  50655  fuco22  50676  fuco22natlem  50682  functhinclem4  50797  functhincfun  50799  arweuthinc  50879  lanfval  51011  ranfval  51012  islmd  51063  iscmd  51064