Theorem simplrl 775

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5063  f1imass  7022  f1prex  7040  soisoi  7081  riota5f  7142  tfrlem9a  8022  oeeui  8228  oaabs2  8272  omabs  8274  omxpenlem  8618  fopwdom  8625  frfi  8763  marypha1lem  8897  ordiso2  8979  oismo  9004  wemaplem3  9012  cantnf  9156  isinffi  9421  dfac12lem2  9570  dfac12lem3  9571  infxp  9637  infmap2  9640  infpssrlem5  9729  fin23lem11  9739  fin23lem24  9744  fin23lem26  9747  isf32lem2  9776  isf32lem4  9778  fin1a2lem13  9834  fin1a2s  9836  ttukeylem5  9935  fpwwe2lem12  10063  fpwwe2lem13  10064  wunex2  10160  tskord  10202  prlem934  10455  mulcmpblnr  10493  dedekind  10803  addid1  10820  cnegex  10821  negeu  10876  add20  11152  divdivdiv  11341  ltmul12a  11496  lediv12a  11533  cru  11630  uzwo3  12344  xleadd1a  12647  xlemul1a  12682  ixxun  12755  ixxss12  12759  elfz0ubfz0  13012  mulexpz  13470  rpexpmord  13533  leexp1a  13540  expmulnbnd  13597  swrdccatin1  14087  pfxccatin12lem3  14094  pfxccat3  14096  abs3lem  14698  rexanre  14706  cau3lem  14714  lo1bdd2  14881  o1lo1  14894  rlimclim1  14902  rlimclim  14903  lo1resb  14921  o1resb  14923  rlimcn2  14947  o1of2  14969  o1rlimmul  14975  lo1add  14983  lo1mul  14984  isercolllem1  15021  climcau  15027  summolem2  15073  summo  15074  o1fsum  15168  prodmolem2  15289  qredeu  16002  isprm5  16051  pclem  16175  pcqmul  16190  pcexp  16196  pcneg  16210  pcprmpw2  16218  pcadd  16225  prmpwdvds  16240  4sqlem13  16293  vdwlem2  16318  vdwlem7  16323  vdwlem11  16327  vdwlem12  16328  ramval  16344  ramz2  16360  ramcl  16365  prmgaplem6  16392  cshwshashlem2  16430  imasval  16784  imasdsval  16788  mreexexd  16919  issubc3  17119  idfucl  17151  funcres2c  17171  fucpropd  17247  xpcval  17427  prfval  17449  evlfcl  17472  curf12  17477  curf1cl  17478  curf2  17479  curfcl  17482  curfuncf  17488  curf2ndf  17497  hof2val  17506  hofcl  17509  hofpropd  17517  yonedalem4a  17525  yonedainv  17531  poslubmo  17756  posglbmo  17757  isipodrs  17771  acsmapd  17788  acsinfd  17790  ismndd  17933  mndpropd  17936  mhmeql  17990  mndind  17992  frmdup3lem  18031  mhmmnd  18221  issubg4  18298  ssnmz  18318  f1otrspeq  18575  psgneu  18634  sylow2blem3  18747  lsmdisj2  18808  pj1eu  18822  efgredlem  18873  frgpuplem  18898  frgpnabl  18995  dmdprdsplitlem  19159  pgpfac1lem3  19199  pgpfaclem3  19205  ablsimpgcygd  19228  ringpropd  19332  dvdsrtr  19402  islmhm2  19810  lmhmpropd  19845  assapropd  20101  evlslem1  20295  coe1tmmul2  20444  prmirredlem  20640  psgndiflemA  20745  lsmcss  20836  dsmmlss  20888  uvcf1  20936  frlmup1  20942  mamucl  21010  mamuass  21011  mamudi  21012  mamudir  21013  mamuvs1  21014  mamuvs2  21015  mamulid  21050  mamurid  21051  dmatsubcl  21107  dmatmulcl  21109  mdetunilem7  21227  mdetunilem9  21229  cramer0  21299  cpmatmcllem  21326  mat2pmatf1  21337  decpmatmul  21380  pmatcollpw1  21384  pm2mpf1lem  21402  pm2mpmhmlem2  21427  chpidmat  21455  cpmadugsumlemB  21482  cpmadugsumlemC  21483  toponmre  21701  restbas  21766  iscncl  21877  cnpdis  21901  lmcnp  21912  dishaus  21990  cmpcovf  21999  hauscmplem  22014  dfconn2  22027  clsconn  22038  2ndcctbss  22063  1stccnp  22070  islly2  22092  llyidm  22096  cldllycmp  22103  locfincmp  22134  kgentopon  22146  1stckgenlem  22161  ptpjpre1  22179  ptbasfi  22189  txcls  22212  ptpjopn  22220  xkoccn  22227  txcnp  22228  txcmpb  22252  xkoptsub  22262  xkoco2cn  22266  xkoinjcn  22295  qtopcn  22322  qtoprest  22325  regr1lem  22347  regr1lem2  22348  kqreglem1  22349  qtophmeo  22425  fgabs  22487  hauspwpwf1  22595  flimfnfcls  22636  fclscmp  22638  cnpfcf  22649  ptcmplem4  22663  ptcmplem5  22664  cnextfval  22670  cnextfun  22672  tmdgsum2  22704  tsmsval2  22738  utoptop  22843  utop3cls  22860  ismet2  22943  blin  23031  metss2lem  23121  methaus  23130  met1stc  23131  met2ndci  23132  metcnp  23151  metcnpi3  23156  metustto  23163  metustfbas  23167  nlmvscn  23296  nrginvrcn  23301  nghmcn  23354  xrsxmet  23417  reconnlem1  23434  reconn  23436  xrge0tsms  23442  xmetdcn2  23445  metdscn  23464  addcnlem  23472  mulc1cncf  23513  cncfco  23515  cnheiborlem  23558  cnheibor  23559  nmoleub2lem2  23720  ipcn  23849  iscfil3  23876  cfilfcls  23877  iscmet3  23896  caubl  23911  bcthlem5  23931  rrxdstprj1  24012  minveclem3b  24031  minveclem7  24038  pmltpc  24051  ovolshftlem1  24110  ovolscalem1  24114  ioombl1  24163  uniioombllem6  24189  dyadss  24195  dyaddisjlem  24196  dyadmax  24199  opnmbllem  24202  itg1addlem2  24298  itg2seq  24343  bddmulibl  24439  limcfval  24470  ellimc3  24477  limciun  24492  dveflem  24576  rolle  24587  dvlip2  24592  c1liplem1  24593  dvgt0lem1  24599  dvgt0  24601  dvlt0  24602  dvne0  24608  dvcnvre  24616  dvfsumrlimge0  24627  ftc1lem6  24638  itgsubst  24646  mdegmullem  24672  ply1domn  24717  fta1g  24761  fta1b  24763  dgrlem  24819  coeid  24828  plydivalg  24888  aannenlem1  24917  aalioulem6  24926  ulmcn  24987  mtestbdd  24993  abelthlem8  25027  efif1olem4  25129  chordthm  25415  xrlimcnp  25546  lgamgulmlem5  25610  isppw2  25692  fsumvma2  25790  perfectlem2  25806  lgsdilem  25900  lgsquad2lem2  25961  lgsquad3  25963  2sqlem5  25998  2sqlem9  26003  rpvmasumlem  26063  dchrisum0flb  26086  pntpbnd  26164  pntibndlem3  26168  pntlem3  26185  pntleml  26187  tgjustc1  26261  tgjustc2  26262  tgbtwnconn1lem3  26360  legtrid  26377  tglinethru  26422  tglnpt2  26427  tglineintmo  26428  mirreu3  26440  perpcom  26499  footexALT  26504  footex  26507  mideu  26524  opphllem1  26533  lnopp2hpgb  26549  axsegcon  26713  axpasch  26727  axeuclidlem  26748  ecgrtg  26769  elntg  26770  eengtrkg  26772  upgr1eopALT  26902  usgredg4  26999  usgr1eop  27032  usgr1v  27038  subuhgr  27068  subumgr  27070  subusgr  27071  nbuhgr2vtx1edgb  27134  wwlksnext  27671  usgr2wspthon  27744  clwlkclwwlkf1  27788  clwwisshclwwslem  27792  n4cyclfrgr  28070  dlwwlknondlwlknonf1o  28144  vacn  28471  ubthlem1  28647  ubthlem3  28649  minvecolem7  28660  chocunii  29078  pjhthmo  29079  pjhthlem2  29169  nmopub2tALT  29686  nmfnleub2  29703  kbass5  29897  mdslmd1lem1  30102  mdslmd1lem2  30103  mdsymlem5  30184  fcobij  30458  xrofsup  30492  xrge0tsmsd  30692  symgcntz  30729  archiabllem2a  30823  gsumvsca1  30854  gsumvsca2  30855  isarchiofld  30890  prmidl2  30958  ssmxidl  30979  smatrcl  31061  reff  31103  ordtconnlem1  31167  qqhval2  31223  esumpcvgval  31337  imambfm  31520  ballotlemsf1o  31771  signstfvneq0  31842  pconnconn  32478  connpconn  32482  cvmliftmo  32531  cvmlift2lem10  32559  cvmlift2lem12  32561  cvmlift3lem7  32572  mrsubff1  32761  msubff1  32803  frpomin  33078  noprefixmo  33202  noetalem3  33219  slerec  33277  ifscgr  33505  cgrxfr  33516  btwnconn1lem13  33560  ellines  33613  unblimceq0lem  33845  unbdqndv2  33850  matunitlindflem1  34903  poimirlem4  34911  poimirlem13  34920  poimirlem14  34921  heicant  34942  opnmbllem0  34943  mblfinlem3  34946  itg2addnclem  34958  itg2addnc  34961  ftc1cnnc  34981  sstotbnd  35068  cntotbnd  35089  ismtyima  35096  heibor1lem  35102  heiborlem10  35113  bfp  35117  rrncmslem  35125  islshpsm  36131  lsatcmp  36154  islshpat  36168  lfl0f  36220  iscvlat2N  36475  ishlat3N  36505  3dim1  36618  islvol5  36730  lvoli2  36732  lncvrelatN  36932  lncmp  36934  paddasslem10  36980  pclfinclN  37101  pexmidlem8N  37128  idltrn  37301  cdleme42keg  37637  cdleme42mgN  37639  cdlemf2  37713  cdlemg2cex  37742  trlcoat  37874  tendoex  38126  erngdvlem4  38142  erngdvlem4-rN  38150  dialss  38197  dibglbN  38317  diblss  38321  dihlsscpre  38385  dihglblem2aN  38444  dihglblem4  38448  dihglblem5  38449  dih1dimatlem  38480  dihglblem6  38491  lcfl7N  38652  lcfrlem9  38701  mapdh9a  38940  hdmapglem7  39080  renegeulemv  39218  remulinvcom  39268  prjspertr  39275  prjspreln0  39279  isnacs3  39327  nacsfix  39329  mzpsubst  39365  eldioph2lem2  39378  eldioph2  39379  eldioph2b  39380  diophin  39389  diophun  39390  rencldnfilem  39437  irrapxlem3  39441  irrapxlem5  39443  pell1234qrreccl  39471  pell1234qrmulcl  39472  pell1qrge1  39487  pell1qrgaplem  39490  monotuz  39558  monotoddzzfi  39559  acongtr  39595  acongrep  39597  jm2.26a  39617  jm2.26lem3  39618  jm2.26  39619  jm2.27b  39623  jm2.27  39625  wepwsolem  39662  fnwe2lem2  39671  hbtlem5  39748  hbt  39750  mpaaeu  39770  rfovcnvf1od  40370  mnurndlem1  40637  fnchoice  41306  rfcnnnub  41313  disjxp1  41351  ioondisj2  41787  iccintsng  41819  fprodcn  41901  lptioo2  41932  lptioo1  41933  limclner  41952  dvdsn1add  42244  stoweidlem14  42319  stoweidlem27  42332  stoweidlem34  42339  stoweidlem49  42354  stoweidlem56  42361  fourierdlem87  42498  iundjiun  42762  ismeannd  42769  hoidmvle  42902  prproropf1olem2  43686  perfectALTVlem2  43907  mogoldbb  43970  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  mgmhmeql  44090  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  mndpsuppss  44439  lindslinindsimp2lem5  44537  itscnhlinecirc02p  44792