Theorem simplrl 782

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  disjxiun  5076  frpomin  6298  f1imass  7215  f1prex  7235  soisoi  7279  riota5f  7348  frxp3  8098  xpord3pred  8099  tfrlem9a  8322  oeeui  8535  oaabs2  8582  omabs  8584  naddssim  8618  omxpenlem  9013  fopwdom  9020  frfi  9192  marypha1lem  9343  ordiso2  9427  oismo  9452  wemaplem3  9460  cantnf  9612  ttrclss  9639  isinffi  9914  dfac12lem2  10065  dfac12lem3  10066  infxp  10134  infmap2  10137  infpssrlem5  10227  fin23lem11  10237  fin23lem24  10242  fin23lem26  10245  isf32lem2  10274  isf32lem4  10276  fin1a2lem13  10332  fin1a2s  10334  ttukeylem5  10433  fpwwe2lem11  10562  fpwwe2lem12  10563  wunex2  10659  tskord  10701  prlem934  10954  mulcmpblnr  10992  dedekind  11307  addrid  11324  cnegex  11325  negeu  11381  add20  11660  divdivdiv  11854  ltmul12a  12009  lediv12a  12047  cru  12149  uzwo3  12891  xleadd1a  13203  xlemul1a  13238  ixxun  13312  ixxss12  13316  elfz0ubfz0  13584  mulexpz  14062  rpexpmord  14128  leexp1a  14135  expmulnbnd  14195  swrdccatin1  14685  pfxccatin12lem3  14692  pfxccat3  14694  abs3lem  15299  rexanre  15307  cau3lem  15315  lo1bdd2  15484  o1lo1  15497  rlimclim1  15505  rlimclim  15506  lo1resb  15524  o1resb  15526  rlimcn3  15550  o1of2  15573  o1rlimmul  15579  lo1add  15587  lo1mul  15588  isercolllem1  15625  climcau  15631  summolem2  15676  summo  15677  o1fsum  15774  prodmolem2  15898  qredeu  16625  isprm5  16675  pclem  16807  pcqmul  16822  pcexp  16828  pcneg  16843  pcprmpw2  16851  pcadd  16858  prmpwdvds  16873  4sqlem13  16926  vdwlem2  16951  vdwlem7  16956  vdwlem11  16960  vdwlem12  16961  ramval  16977  ramz2  16993  ramcl  16998  prmgaplem6  17025  cshwshashlem2  17065  imasval  17473  imasdsval  17477  mreexexd  17612  issubc3  17814  idfucl  17846  funcres2c  17868  fucpropd  17945  xpcval  18141  prfval  18163  evlfcl  18186  curf12  18191  curf1cl  18192  curf2  18193  curfcl  18196  curfuncf  18202  curf2ndf  18211  hof2val  18220  hofcl  18223  hofpropd  18231  yonedalem4a  18239  yonedainv  18245  poslubmo  18373  posglbmo  18374  isipodrs  18501  acsmapd  18518  acsinfd  18520  chnpof1  18594  mgmhmeql  18682  sgrppropd  18697  ismndd  18722  mndpropd  18725  mndpsuppss  18731  mhmeql  18792  mndind  18794  frmdup3lem  18832  mhmmnd  19038  issubg4  19119  ssnmz  19139  f1otrspeq  19420  psgneu  19479  sylow2blem3  19595  lsmdisj2  19655  pj1eu  19669  efgredlem  19720  frgpuplem  19745  frgpnabl  19848  dmdprdsplitlem  20012  pgpfac1lem3  20052  pgpfaclem3  20058  ablsimpgcygd  20081  rngpropd  20153  ringpropd  20267  dvdsrtr  20346  rngcinv  20616  ringcinv  20650  islmhm2  21035  lmhmpropd  21070  prmirredlem  21454  psgndiflemA  21583  lsmcss  21674  dsmmlss  21726  uvcf1  21774  frlmup1  21780  assapropd  21853  evlslem1  22065  coe1tmmul2  22269  mamucl  22391  mamuass  22392  mamudi  22393  mamudir  22394  mamuvs1  22395  mamuvs2  22396  mamulid  22431  mamurid  22432  dmatsubcl  22488  dmatmulcl  22490  mdetunilem7  22608  mdetunilem9  22610  cramer0  22680  cpmatmcllem  22708  mat2pmatf1  22719  decpmatmul  22762  pmatcollpw1  22766  pm2mpf1lem  22784  pm2mpmhmlem2  22809  chpidmat  22837  cpmadugsumlemB  22864  cpmadugsumlemC  22865  toponmre  23083  restbas  23148  iscncl  23259  cnpdis  23283  lmcnp  23294  dishaus  23372  cmpcovf  23381  hauscmplem  23396  dfconn2  23409  clsconn  23420  2ndcctbss  23445  1stccnp  23452  islly2  23474  llyidm  23478  cldllycmp  23485  locfincmp  23516  kgentopon  23528  1stckgenlem  23543  ptpjpre1  23561  ptbasfi  23571  txcls  23594  ptpjopn  23602  xkoccn  23609  txcnp  23610  txcmpb  23634  xkoptsub  23644  xkoco2cn  23648  xkoinjcn  23677  qtopcn  23704  qtoprest  23707  regr1lem  23729  regr1lem2  23730  kqreglem1  23731  qtophmeo  23807  fgabs  23869  hauspwpwf1  23977  flimfnfcls  24018  fclscmp  24020  cnpfcf  24031  ptcmplem4  24045  ptcmplem5  24046  cnextfval  24052  cnextfun  24054  tmdgsum2  24086  tsmsval2  24120  utoptop  24224  utop3cls  24241  ismet2  24323  blin  24411  metss2lem  24501  methaus  24510  met1stc  24511  met2ndci  24512  metcnp  24531  metcnpi3  24536  metustto  24543  metustfbas  24547  nlmvscn  24677  nrginvrcn  24682  nghmcn  24735  xrsxmet  24800  reconnlem1  24817  reconn  24819  xrge0tsms  24825  xmetdcn2  24828  metdscn  24847  addcnlem  24855  mulc1cncf  24897  cncfco  24899  cnheiborlem  24946  cnheibor  24947  nmoleub2lem2  25108  ipcn  25238  iscfil3  25265  cfilfcls  25266  iscmet3  25285  caubl  25300  bcthlem5  25320  rrxdstprj1  25401  minveclem3b  25420  minveclem7  25427  pmltpc  25442  ovolshftlem1  25501  ovolscalem1  25505  ioombl1  25554  uniioombllem6  25580  dyadss  25586  dyaddisjlem  25587  dyadmax  25590  opnmbllem  25593  itg1addlem2  25689  itg2seq  25734  bddmulibl  25831  limcfval  25864  ellimc3  25871  limciun  25886  dveflem  25971  rolle  25982  dvlip2  25987  c1liplem1  25988  dvgt0lem1  25994  dvgt0  25996  dvlt0  25997  dvne0  26003  dvcnvre  26011  dvfsumrlimge0  26022  ftc1lem6  26033  itgsubst  26041  mdegmullem  26068  ply1domn  26114  fta1g  26160  fta1b  26162  dgrlem  26219  coeid  26228  plydivalg  26290  aannenlem1  26319  aalioulem6  26328  ulmcn  26389  mtestbdd  26395  abelthlem8  26429  efif1olem4  26534  chordthm  26826  xrlimcnp  26957  lgamgulmlem5  27021  isppw2  27103  fsumvma2  27202  perfectlem2  27218  lgsdilem  27312  lgsquad2lem2  27373  lgsquad3  27375  2sqlem5  27410  2sqlem9  27415  rpvmasumlem  27475  dchrisum0flb  27498  pntpbnd  27576  pntibndlem3  27580  pntlem3  27597  pntleml  27599  nosupbday  27694  noinfbday  27709  noetasuplem4  27725  noetainflem4  27729  noetalem1  27730  lesrec  27816  madebdaylemlrcut  27916  bdayons  28293  n0fincut  28372  eucliddivs  28393  bdayfinbndlem1  28484  remulscllem2  28518  tgjustc1  28568  tgjustc2  28569  tgbtwnconn1lem3  28667  legtrid  28684  tglinethru  28729  tglnpt2  28734  tglineintmo  28735  mirreu3  28747  perpcom  28806  footexALT  28811  footex  28814  mideu  28831  opphllem1  28840  lnopp2hpgb  28856  axsegcon  29021  axpasch  29035  axeuclidlem  29056  ecgrtg  29077  elntg  29078  eengtrkg  29080  upgr1eopALT  29211  usgredg4  29311  usgr1eop  29344  usgr1v  29350  subuhgr  29380  subumgr  29382  subusgr  29383  nbuhgr2vtx1edgb  29446  wwlksnext  29986  usgr2wspthon  30061  clwlkclwwlkf1  30105  clwwisshclwwslem  30109  n4cyclfrgr  30386  dlwwlknondlwlknonf1o  30460  vacn  30790  ubthlem1  30966  ubthlem3  30968  minvecolem7  30979  chocunii  31397  pjhthmo  31398  pjhthlem2  31488  nmopub2tALT  32005  nmfnleub2  32022  kbass5  32216  mdslmd1lem1  32421  mdslmd1lem2  32422  mdsymlem5  32503  fcobij  32819  xrofsup  32866  mgcf1o  33089  xrge0tsmsd  33161  symgcntz  33173  archiabllem2a  33282  isarchiofld  33287  gsumvsca1  33314  gsumvsca2  33315  prmidl2  33531  ssmxidl  33564  mplvrpmrhm  33738  constrelextdg2  33938  smatrcl  33987  reff  34030  ordtconnlem1  34115  qqhval2  34173  esumpcvgval  34269  imambfm  34453  ballotlemsf1o  34705  signstfvneq0  34763  pconnconn  35466  connpconn  35470  cvmliftmo  35519  cvmlift2lem10  35547  cvmlift2lem12  35549  cvmlift3lem7  35560  mrsubff1  35749  msubff1  35791  ifscgr  36279  cgrxfr  36290  btwnconn1lem13  36334  ellines  36387  weiunso  36701  weiunfr  36702  unblimceq0lem  36819  unbdqndv2  36824  irrdiff  37693  qdiff  37694  matunitlindflem1  37990  poimirlem4  37998  poimirlem13  38007  poimirlem14  38008  heicant  38029  opnmbllem0  38030  mblfinlem3  38033  itg2addnclem  38045  itg2addnc  38048  ftc1cnnc  38066  sstotbnd  38149  cntotbnd  38170  ismtyima  38177  heibor1lem  38183  heiborlem10  38194  bfp  38198  rrncmslem  38206  islshpsm  39479  lsatcmp  39502  islshpat  39516  lfl0f  39568  iscvlat2N  39823  ishlat3N  39853  3dim1  39966  islvol5  40078  lvoli2  40080  lncvrelatN  40280  lncmp  40282  paddasslem10  40328  pclfinclN  40449  pexmidlem8N  40476  idltrn  40649  cdleme42keg  40985  cdleme42mgN  40987  cdlemf2  41061  cdlemg2cex  41090  trlcoat  41222  tendoex  41474  erngdvlem4  41490  erngdvlem4-rN  41498  dialss  41545  dibglbN  41665  diblss  41669  dihlsscpre  41733  dihglblem2aN  41792  dihglblem4  41796  dihglblem5  41797  dih1dimatlem  41828  dihglblem6  41839  lcfl7N  42000  lcfrlem9  42049  mapdh9a  42288  hdmapglem7  42428  aks4d1p8  42579  isprimroot  42585  evl1gprodd  42609  hashnexinjle  42621  deg1gprod  42632  sticksstones22  42660  grpods  42686  renegeulemv  42852  sn-subeu  42911  remulinvcom  42917  imacrhmcl  43011  fidomncyc  43028  fsuppind  43047  prjspertr  43062  prjspreln0  43066  flt4lem7  43116  nna4b4nsq  43117  isnacs3  43166  nacsfix  43168  mzpsubst  43204  eldioph2lem2  43217  eldioph2  43218  eldioph2b  43219  diophin  43228  diophun  43229  rencldnfilem  43272  irrapxlem3  43276  irrapxlem5  43278  pell1234qrreccl  43306  pell1234qrmulcl  43307  pell1qrge1  43322  pell1qrgaplem  43325  monotuz  43393  monotoddzzfi  43394  acongtr  43430  acongrep  43432  jm2.26a  43452  jm2.26lem3  43453  jm2.26  43454  jm2.27b  43458  jm2.27  43460  wepwsolem  43494  fnwe2lem2  43503  hbtlem5  43580  hbt  43582  mpaaeu  43602  cantnftermord  43772  cantnfresb  43776  omabs2  43784  tfsconcatun  43789  tfsconcatfn  43790  tfsconcatfv1  43791  tfsconcatfv2  43792  tfsconcatfv  43793  tfsconcatrn  43794  naddcnff  43814  oaun3lem1  43826  rfovcnvf1od  44455  mnurndlem1  44732  fnchoice  45484  rfcnnnub  45491  disjxp1  45524  ioondisj2  45945  iccintsng  45975  fprodcn  46052  lptioo2  46083  lptioo1  46084  limclner  46101  dvdsn1add  46389  stoweidlem14  46464  stoweidlem27  46477  stoweidlem34  46484  stoweidlem49  46499  stoweidlem56  46506  fourierdlem87  46643  iundjiun  46910  ismeannd  46917  hoidmvle  47050  prproropf1olem2  47986  nprmmul2  48010  perfectALTVlem2  48220  mogoldbb  48283  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  grimgrtri  48447  isubgr3stgrlem6  48469  rngcinvALTV  48774  ringcinvALTV  48808  lindslinindsimp2lem5  48960  itscnhlinecirc02p  49283  toslat  49479  iinfssclem3  49553  iinfssc  49554  iinfsubc  49555  discsubc  49561  iinfconstbas  49563  imasubc3  49653  upciclem4  49666  natoppf  49726  tposcurf1  49796  fucofvalg  49815  fuco22  49836  fuco22natlem  49842  functhinclem4  49944  functhincfun  49946  arweuthinc  50026  lanfval  50110  ranfval  50111  islmd  50162  iscmd  50163