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  5104  frpomin  6342  f1imass  7265  f1prex  7289  soisoi  7333  riota5f  7402  frxp3  8153  xpord3pred  8154  tfrlem9a  8379  oeeui  8594  oaabs2  8641  omabs  8643  naddssim  8678  omxpenlem  9080  fopwdom  9087  frfi  9259  marypha1lem  9407  ordiso2  9491  oismo  9516  wemaplem3  9524  cantnf  9676  ttrclss  9703  isinffi  10001  dfac12lem2  10151  dfac12lem3  10152  infxp  10220  infmap2  10223  infpssrlem5  10313  fin23lem11  10323  fin23lem24  10328  fin23lem26  10331  isf32lem2  10360  isf32lem4  10362  fin1a2lem13  10418  fin1a2s  10420  ttukeylem5  10519  fpwwe2lem11  10654  fpwwe2lem12  10655  wunex2  10751  tskord  10793  prlem934  11046  mulcmpblnr  11084  dedekind  11401  addrid  11418  cnegex  11419  negeu  11475  add20  11754  divdivdiv  11944  ltmul12a  12099  lediv12a  12136  cru  12238  uzwo3  12996  xleadd1a  13309  xlemul1a  13344  ixxun  13418  ixxss12  13422  elfz0ubfz0  13691  mulexpz  14170  rpexpmord  14236  leexp1a  14243  expmulnbnd  14303  swrdccatin1  14798  pfxccatin12lem3  14805  pfxccat3  14807  abs3lem  15430  rexanre  15438  cau3lem  15446  lo1bdd2  15615  o1lo1  15628  rlimclim1  15636  rlimclim  15637  lo1resb  15655  o1resb  15657  rlimcn3  15681  o1of2  15704  o1rlimmul  15710  lo1add  15718  lo1mul  15719  isercolllem1  15756  climcau  15762  summolem2  15806  summo  15807  o1fsum  15904  prodmolem2  16028  qredeu  16754  isprm5  16804  pclem  16936  pcqmul  16951  pcexp  16957  pcneg  16972  pcprmpw2  16980  pcadd  16987  prmpwdvds  17002  4sqlem13  17055  vdwlem2  17080  vdwlem7  17085  vdwlem11  17089  vdwlem12  17090  ramval  17106  ramz2  17122  ramcl  17127  prmgaplem6  17154  cshwshashlem2  17194  imasval  17603  imasdsval  17607  mreexexd  17742  issubc3  17944  idfucl  17976  funcres2c  17998  fucpropd  18075  xpcval  18271  prfval  18293  evlfcl  18316  curf12  18321  curf1cl  18322  curf2  18323  curfcl  18326  curfuncf  18332  curf2ndf  18341  hof2val  18350  hofcl  18353  hofpropd  18361  yonedalem4a  18369  yonedainv  18375  poslubmo  18503  posglbmo  18504  isipodrs  18631  acsmapd  18648  acsinfd  18650  chnpof1  18724  mgmhmeql  18824  sgrppropd  18839  ismndd  18865  mndpropd  18870  mndpsuppss  18878  mhmeql  18941  mndind  18943  frmdup3lem  18981  mhmmnd  19193  issubg4  19275  ssnmz  19295  f1otrspeq  19580  psgneu  19639  sylow2blem3  19755  lsmdisj2  19815  pj1eu  19829  efgredlem  19880  frgpuplem  19905  frgpnabl  20008  dmdprdsplitlem  20172  pgpfac1lem3  20212  pgpfaclem3  20218  ablsimpgcygd  20241  rngpropd  20315  ringpropd  20436  dvdsrtr  20515  rngcinv  20805  ringcinv  20839  islmhm2  21228  lmhmpropd  21263  prmidl2  21535  prmirredlem  21691  psgndiflemA  21820  lsmcss  21911  dsmmlss  21963  uvcf1  22011  frlmup1  22017  assapropd  22092  evlslem1  22304  coe1tmmul2  22508  mamucl  22629  mamuass  22630  mamudi  22631  mamudir  22632  mamuvs1  22633  mamuvs2  22634  mamulid  22669  mamurid  22670  dmatsubcl  22726  dmatmulcl  22728  mdetunilem7  22846  mdetunilem9  22848  matunitlindflem1  22907  cramer0  22921  cpmatmcllem  22949  mat2pmatf1  22960  decpmatmul  23003  pmatcollpw1  23007  pm2mpf1lem  23025  pm2mpmhmlem2  23050  chpidmat  23078  cpmadugsumlemB  23105  cpmadugsumlemC  23106  toponmre  23324  restbas  23389  iscncl  23500  cnpdis  23524  lmcnp  23535  dishaus  23613  cmpcovf  23622  hauscmplem  23637  dfconn2  23650  clsconn  23661  2ndcctbss  23687  1stccnp  23694  islly2  23716  llyidm  23720  cldllycmp  23727  locfincmp  23758  kgentopon  23770  1stckgenlem  23785  ptpjpre1  23803  ptbasfi  23813  txcls  23836  ptpjopn  23844  xkoccn  23851  txcnp  23852  txcmpb  23876  xkoptsub  23886  xkoco2cn  23890  xkoinjcn  23919  qtopcn  23946  qtoprest  23949  regr1lem  23971  regr1lem2  23972  kqreglem1  23973  qtophmeo  24049  fgabs  24111  hauspwpwf1  24219  flimfnfcls  24260  fclscmp  24262  cnpfcf  24273  ptcmplem4  24287  ptcmplem5  24288  cnextfval  24294  cnextfun  24296  tmdgsum2  24328  tsmsval2  24362  utoptop  24466  utop3cls  24483  ismet2  24565  blin  24653  metss2lem  24743  methaus  24752  met1stc  24753  met2ndci  24754  metcnp  24773  metcnpi3  24778  metustto  24785  metustfbas  24789  nlmvscn  24919  nrginvrcn  24924  nghmcn  24977  xrsxmet  25042  reconnlem1  25059  reconn  25061  xrge0tsms  25067  xmetdcn2  25070  metdscn  25089  addcnlem  25097  mulc1cncf  25139  cncfco  25141  cnheiborlem  25188  cnheibor  25189  nmoleub2lem2  25350  ipcn  25480  iscfil3  25507  cfilfcls  25508  iscmet3  25527  caubl  25542  bcthlem5  25562  rrxdstprj1  25643  minveclem3b  25662  minveclem7  25669  pmltpc  25684  ovolshftlem1  25743  ovolscalem1  25747  ioombl1  25796  uniioombllem6  25822  dyadss  25828  dyaddisjlem  25829  dyadmax  25832  opnmbllem  25835  itg1addlem2  25931  itg2seq  25976  bddmulibl  26073  limcfval  26106  ellimc3  26113  limciun  26128  dveflem  26213  rolle  26224  dvlip2  26229  c1liplem1  26230  dvgt0lem1  26236  dvgt0  26238  dvlt0  26239  dvne0  26245  dvcnvre  26253  dvfsumrlimge0  26264  ftc1lem6  26275  itgsubst  26283  mdegmullem  26310  ply1domn  26356  fta1g  26402  fta1b  26404  dgrlem  26462  coeid  26471  plydivalg  26536  aannenlem1  26571  aalioulem6  26580  ulmcn  26642  mtestbdd  26648  abelthlem8  26682  efif1olem4  26790  chordthm  27082  xrlimcnp  27213  lgamgulmlem5  27277  isppw2  27359  fsumvma2  27458  perfectlem2  27474  lgsdilem  27568  lgsquad2lem2  27629  lgsquad3  27631  2sqlem5  27666  2sqlem9  27671  rpvmasumlem  27731  dchrisum0flb  27754  pntpbnd  27832  pntibndlem3  27836  pntlem3  27853  pntleml  27855  nosupbday  27949  noinfbday  27964  noetasuplem4  27980  noetainflem4  27984  noetalem1  27985  lesrec  28072  madebdaylemlrcut  28172  bdayons  28549  n0fincut  28628  eucliddivs  28649  bdayfinbndlem1  28740  remulscllem2  28774  tgjustc1  28824  tgjustc2  28825  tgbtwnconn1lem3  28924  legtrid  28941  tglinethru  28991  tglineintmo  28997  tglnpt2  29008  mirreu3  29013  perpcom  29075  footexALT  29080  footex  29083  mideu  29101  opphllem1  29110  lnopp2hpgb  29128  axsegcon  29392  axpasch  29406  axeuclidlem  29427  ecgrtg  29448  elntg  29449  eengtrkg  29451  upgr1eopALT  29582  usgredg4  29685  usgr1eop  29718  usgr1v  29724  subuhgr  29754  subumgr  29756  subusgr  29757  nbuhgr2vtx1edgb  29820  wwlksnext  30369  usgr2wspthon  30444  clwlkclwwlkf1  30488  clwwisshclwwslem  30492  n4cyclfrgr  30779  dlwwlknondlwlknonf1o  30853  vacn  31183  ubthlem1  31359  ubthlem3  31361  minvecolem7  31372  chocunii  31790  pjhthmo  31791  pjhthlem2  31881  nmopub2tALT  32398  nmfnleub2  32415  kbass5  32609  mdslmd1lem1  32814  mdslmd1lem2  32815  mdsymlem5  32896  fcobij  33199  xrofsup  33246  mgcf1o  33451  xrge0tsmsd  33521  symgcntz  33533  archiabllem2a  33642  isarchiofld  33647  gsumvsca1  33674  gsumvsca2  33675  ssmxidl  33885  mplvrpmrhm  34065  constrelextdg2  34265  smatrcl  34314  reff  34357  ordtconnlem1  34442  qqhval2  34500  esumpcvgval  34596  imambfm  34781  ballotlemsf1o  35033  signstfvneq0  35088  pconnconn  35818  connpconn  35822  cvmliftmo  35871  cvmlift2lem10  35899  cvmlift2lem12  35901  cvmlift3lem7  35912  mrsubff1  36101  msubff1  36143  ifscgr  36632  cgrxfr  36643  btwnconn1lem13  36687  ellines  36740  nmuladdss  36801  nadddilem4  36811  weiunso  37093  weiunfr  37094  unblimceq0lem  37211  unbdqndv2  37216  irrdiff  38086  qdiff  38087  poimirlem4  38381  poimirlem13  38390  poimirlem14  38391  heicant  38412  opnmbllem0  38413  mblfinlem3  38416  itg2addnclem  38428  itg2addnc  38431  ftc1cnnc  38449  sstotbnd  38533  cntotbnd  38554  ismtyima  38561  heibor1lem  38567  heiborlem10  38578  bfp  38582  rrncmslem  38590  islshpsm  39861  lsatcmp  39884  islshpat  39898  lfl0f  39950  iscvlat2N  40205  ishlat3N  40235  3dim1  40348  islvol5  40460  lvoli2  40462  lncvrelatN  40662  lncmp  40664  paddasslem10  40710  pclfinclN  40831  pexmidlem8N  40858  idltrn  41031  cdleme42keg  41367  cdleme42mgN  41369  cdlemf2  41443  cdlemg2cex  41472  trlcoat  41604  tendoex  41856  erngdvlem4  41872  erngdvlem4-rN  41880  dialss  41927  dibglbN  42047  diblss  42051  dihlsscpre  42115  dihglblem2aN  42174  dihglblem4  42178  dihglblem5  42179  dih1dimatlem  42210  dihglblem6  42221  lcfl7N  42382  lcfrlem9  42431  mapdh9a  42670  hdmapglem7  42810  aks4d1p8  42961  isprimroot  42967  evl1gprodd  42991  hashnexinjle  43003  deg1gprod  43014  sticksstones22  43042  grpods  43068  renegeulemv  43251  sn-subeu  43310  remulinvcom  43316  imacrhmcl  43410  fidomncyc  43425  fsuppind  43444  prjspertr  43459  prjspreln0  43463  flt4lem7  43513  nna4b4nsq  43514  isnacs3  43563  nacsfix  43565  mzpsubst  43601  eldioph2lem2  43614  eldioph2  43615  eldioph2b  43616  diophin  43625  diophun  43626  rencldnfilem  43669  irrapxlem3  43673  irrapxlem5  43675  pell1234qrreccl  43703  pell1234qrmulcl  43704  pell1qrge1  43719  pell1qrgaplem  43722  monotuz  43790  monotoddzzfi  43791  acongtr  43827  acongrep  43829  jm2.26a  43849  jm2.26lem3  43850  jm2.26  43851  jm2.27b  43855  jm2.27  43857  wepwsolem  43891  fnwe2lem2  43900  hbtlem5  43977  hbt  43979  mpaaeu  43999  cantnftermord  44169  cantnfresb  44173  omabs2  44181  tfsconcatun  44186  tfsconcatfn  44187  tfsconcatfv1  44188  tfsconcatfv2  44189  tfsconcatfv  44190  tfsconcatrn  44191  naddcnff  44211  oaun3lem1  44223  rfovcnvf1od  44852  mnurndlem1  45113  fnchoice  45871  rfcnnnub  45878  disjxp1  45911  ioondisj2  46331  iccintsng  46361  fprodcn  46438  lptioo2  46469  lptioo1  46470  limclner  46487  dvdsn1add  46775  stoweidlem14  46850  stoweidlem27  46863  stoweidlem34  46870  stoweidlem49  46885  stoweidlem56  46892  fourierdlem87  47029  iundjiun  47296  ismeannd  47303  hoidmvle  47436  prproropf1olem2  48412  nprmmul2  48436  perfectALTVlem2  48646  mogoldbb  48709  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  grimgrtri  48873  isubgr3stgrlem6  48895  rngcinvALTV  49199  ringcinvALTV  49233  lindslinindsimp2lem5  49400  itscnhlinecirc02p  49723  toslat  49916  iinfssclem3  49990  iinfssc  49991  iinfsubc  49992  discsubc  49998  iinfconstbas  50000  imasubc3  50090  upciclem4  50103  natoppf  50163  tposcurf1  50233  fucofvalg  50252  fuco22  50273  fuco22natlem  50279  functhinclem4  50381  functhincfun  50383  arweuthinc  50463  lanfval  50547  ranfval  50548  islmd  50599  iscmd  50600