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  5065  f1imass  7024  f1prex  7042  soisoi  7083  riota5f  7144  tfrlem9a  8024  oeeui  8230  oaabs2  8274  omabs  8276  omxpenlem  8620  fopwdom  8627  frfi  8765  marypha1lem  8899  ordiso2  8981  oismo  9006  wemaplem3  9014  cantnf  9158  isinffi  9423  dfac12lem2  9572  dfac12lem3  9573  infxp  9639  infmap2  9642  infpssrlem5  9731  fin23lem11  9741  fin23lem24  9746  fin23lem26  9749  isf32lem2  9778  isf32lem4  9780  fin1a2lem13  9836  fin1a2s  9838  ttukeylem5  9937  fpwwe2lem12  10065  fpwwe2lem13  10066  wunex2  10162  tskord  10204  prlem934  10457  mulcmpblnr  10495  dedekind  10805  addid1  10822  cnegex  10823  negeu  10878  add20  11154  divdivdiv  11343  ltmul12a  11498  lediv12a  11535  cru  11632  uzwo3  12346  xleadd1a  12649  xlemul1a  12684  ixxun  12757  ixxss12  12761  elfz0ubfz0  13014  mulexpz  13472  rpexpmord  13535  leexp1a  13542  expmulnbnd  13599  swrdccatin1  14089  pfxccatin12lem3  14096  pfxccat3  14098  abs3lem  14700  rexanre  14708  cau3lem  14716  lo1bdd2  14883  o1lo1  14896  rlimclim1  14904  rlimclim  14905  lo1resb  14923  o1resb  14925  rlimcn2  14949  o1of2  14971  o1rlimmul  14977  lo1add  14985  lo1mul  14986  isercolllem1  15023  climcau  15029  summolem2  15075  summo  15076  o1fsum  15170  prodmolem2  15291  qredeu  16004  isprm5  16053  pclem  16177  pcqmul  16192  pcexp  16198  pcneg  16212  pcprmpw2  16220  pcadd  16227  prmpwdvds  16242  4sqlem13  16295  vdwlem2  16320  vdwlem7  16325  vdwlem11  16329  vdwlem12  16330  ramval  16346  ramz2  16362  ramcl  16367  prmgaplem6  16394  cshwshashlem2  16432  imasval  16786  imasdsval  16790  mreexexd  16921  issubc3  17121  idfucl  17153  funcres2c  17173  fucpropd  17249  xpcval  17429  prfval  17451  evlfcl  17474  curf12  17479  curf1cl  17480  curf2  17481  curfcl  17484  curfuncf  17490  curf2ndf  17499  hof2val  17508  hofcl  17511  hofpropd  17519  yonedalem4a  17527  yonedainv  17533  poslubmo  17758  posglbmo  17759  isipodrs  17773  acsmapd  17790  acsinfd  17792  ismndd  17935  mndpropd  17938  mhmeql  17992  mndind  17994  frmdup3lem  18033  mhmmnd  18223  issubg4  18300  ssnmz  18320  f1otrspeq  18577  psgneu  18636  sylow2blem3  18749  lsmdisj2  18810  pj1eu  18824  efgredlem  18875  frgpuplem  18900  frgpnabl  18997  dmdprdsplitlem  19161  pgpfac1lem3  19201  pgpfaclem3  19207  ablsimpgcygd  19230  ringpropd  19334  dvdsrtr  19404  islmhm2  19812  lmhmpropd  19847  assapropd  20103  evlslem1  20297  coe1tmmul2  20446  prmirredlem  20642  psgndiflemA  20747  lsmcss  20838  dsmmlss  20890  uvcf1  20938  frlmup1  20944  mamucl  21012  mamuass  21013  mamudi  21014  mamudir  21015  mamuvs1  21016  mamuvs2  21017  mamulid  21052  mamurid  21053  dmatsubcl  21109  dmatmulcl  21111  mdetunilem7  21229  mdetunilem9  21231  cramer0  21301  cpmatmcllem  21328  mat2pmatf1  21339  decpmatmul  21382  pmatcollpw1  21386  pm2mpf1lem  21404  pm2mpmhmlem2  21429  chpidmat  21457  cpmadugsumlemB  21484  cpmadugsumlemC  21485  toponmre  21703  restbas  21768  iscncl  21879  cnpdis  21903  lmcnp  21914  dishaus  21992  cmpcovf  22001  hauscmplem  22016  dfconn2  22029  clsconn  22040  2ndcctbss  22065  1stccnp  22072  islly2  22094  llyidm  22098  cldllycmp  22105  locfincmp  22136  kgentopon  22148  1stckgenlem  22163  ptpjpre1  22181  ptbasfi  22191  txcls  22214  ptpjopn  22222  xkoccn  22229  txcnp  22230  txcmpb  22254  xkoptsub  22264  xkoco2cn  22268  xkoinjcn  22297  qtopcn  22324  qtoprest  22327  regr1lem  22349  regr1lem2  22350  kqreglem1  22351  qtophmeo  22427  fgabs  22489  hauspwpwf1  22597  flimfnfcls  22638  fclscmp  22640  cnpfcf  22651  ptcmplem4  22665  ptcmplem5  22666  cnextfval  22672  cnextfun  22674  tmdgsum2  22706  tsmsval2  22740  utoptop  22845  utop3cls  22862  ismet2  22945  blin  23033  metss2lem  23123  methaus  23132  met1stc  23133  met2ndci  23134  metcnp  23153  metcnpi3  23158  metustto  23165  metustfbas  23169  nlmvscn  23298  nrginvrcn  23303  nghmcn  23356  xrsxmet  23419  reconnlem1  23436  reconn  23438  xrge0tsms  23444  xmetdcn2  23447  metdscn  23466  addcnlem  23474  mulc1cncf  23515  cncfco  23517  cnheiborlem  23560  cnheibor  23561  nmoleub2lem2  23722  ipcn  23851  iscfil3  23878  cfilfcls  23879  iscmet3  23898  caubl  23913  bcthlem5  23933  rrxdstprj1  24014  minveclem3b  24033  minveclem7  24040  pmltpc  24053  ovolshftlem1  24112  ovolscalem1  24116  ioombl1  24165  uniioombllem6  24191  dyadss  24197  dyaddisjlem  24198  dyadmax  24201  opnmbllem  24204  itg1addlem2  24300  itg2seq  24345  bddmulibl  24441  limcfval  24472  ellimc3  24479  limciun  24494  dveflem  24578  rolle  24589  dvlip2  24594  c1liplem1  24595  dvgt0lem1  24601  dvgt0  24603  dvlt0  24604  dvne0  24610  dvcnvre  24618  dvfsumrlimge0  24629  ftc1lem6  24640  itgsubst  24648  mdegmullem  24674  ply1domn  24719  fta1g  24763  fta1b  24765  dgrlem  24821  coeid  24830  plydivalg  24890  aannenlem1  24919  aalioulem6  24928  ulmcn  24989  mtestbdd  24995  abelthlem8  25029  efif1olem4  25131  chordthm  25417  xrlimcnp  25548  lgamgulmlem5  25612  isppw2  25694  fsumvma2  25792  perfectlem2  25808  lgsdilem  25902  lgsquad2lem2  25963  lgsquad3  25965  2sqlem5  26000  2sqlem9  26005  rpvmasumlem  26065  dchrisum0flb  26088  pntpbnd  26166  pntibndlem3  26170  pntlem3  26187  pntleml  26189  tgjustc1  26263  tgjustc2  26264  tgbtwnconn1lem3  26362  legtrid  26379  tglinethru  26424  tglnpt2  26429  tglineintmo  26430  mirreu3  26442  perpcom  26501  footexALT  26506  footex  26509  mideu  26526  opphllem1  26535  lnopp2hpgb  26551  axsegcon  26715  axpasch  26729  axeuclidlem  26750  ecgrtg  26771  elntg  26772  eengtrkg  26774  upgr1eopALT  26904  usgredg4  27001  usgr1eop  27034  usgr1v  27040  subuhgr  27070  subumgr  27072  subusgr  27073  nbuhgr2vtx1edgb  27136  wwlksnext  27673  usgr2wspthon  27746  clwlkclwwlkf1  27790  clwwisshclwwslem  27794  n4cyclfrgr  28072  dlwwlknondlwlknonf1o  28146  vacn  28473  ubthlem1  28649  ubthlem3  28651  minvecolem7  28662  chocunii  29080  pjhthmo  29081  pjhthlem2  29171  nmopub2tALT  29688  nmfnleub2  29705  kbass5  29899  mdslmd1lem1  30104  mdslmd1lem2  30105  mdsymlem5  30186  fcobij  30460  xrofsup  30494  xrge0tsmsd  30694  symgcntz  30731  archiabllem2a  30825  gsumvsca1  30856  gsumvsca2  30857  isarchiofld  30892  prmidl2  30960  ssmxidl  30981  smatrcl  31063  reff  31105  ordtconnlem1  31169  qqhval2  31225  esumpcvgval  31339  imambfm  31522  ballotlemsf1o  31773  signstfvneq0  31844  pconnconn  32480  connpconn  32484  cvmliftmo  32533  cvmlift2lem10  32561  cvmlift2lem12  32563  cvmlift3lem7  32574  mrsubff1  32763  msubff1  32805  frpomin  33080  noprefixmo  33204  noetalem3  33221  slerec  33279  ifscgr  33507  cgrxfr  33518  btwnconn1lem13  33562  ellines  33615  unblimceq0lem  33847  unbdqndv2  33852  matunitlindflem1  34890  poimirlem4  34898  poimirlem13  34907  poimirlem14  34908  heicant  34929  opnmbllem0  34930  mblfinlem3  34933  itg2addnclem  34945  itg2addnc  34948  ftc1cnnc  34968  sstotbnd  35055  cntotbnd  35076  ismtyima  35083  heibor1lem  35089  heiborlem10  35100  bfp  35104  rrncmslem  35112  islshpsm  36118  lsatcmp  36141  islshpat  36155  lfl0f  36207  iscvlat2N  36462  ishlat3N  36492  3dim1  36605  islvol5  36717  lvoli2  36719  lncvrelatN  36919  lncmp  36921  paddasslem10  36967  pclfinclN  37088  pexmidlem8N  37115  idltrn  37288  cdleme42keg  37624  cdleme42mgN  37626  cdlemf2  37700  cdlemg2cex  37729  trlcoat  37861  tendoex  38113  erngdvlem4  38129  erngdvlem4-rN  38137  dialss  38184  dibglbN  38304  diblss  38308  dihlsscpre  38372  dihglblem2aN  38431  dihglblem4  38435  dihglblem5  38436  dih1dimatlem  38467  dihglblem6  38478  lcfl7N  38639  lcfrlem9  38688  mapdh9a  38927  hdmapglem7  39067  renegeulemv  39205  remulinvcom  39255  prjspertr  39262  prjspreln0  39266  isnacs3  39314  nacsfix  39316  mzpsubst  39352  eldioph2lem2  39365  eldioph2  39366  eldioph2b  39367  diophin  39376  diophun  39377  rencldnfilem  39424  irrapxlem3  39428  irrapxlem5  39430  pell1234qrreccl  39458  pell1234qrmulcl  39459  pell1qrge1  39474  pell1qrgaplem  39477  monotuz  39545  monotoddzzfi  39546  acongtr  39582  acongrep  39584  jm2.26a  39604  jm2.26lem3  39605  jm2.26  39606  jm2.27b  39610  jm2.27  39612  wepwsolem  39649  fnwe2lem2  39658  hbtlem5  39735  hbt  39737  mpaaeu  39757  rfovcnvf1od  40357  mnurndlem1  40624  fnchoice  41293  rfcnnnub  41300  disjxp1  41338  ioondisj2  41774  iccintsng  41806  fprodcn  41888  lptioo2  41919  lptioo1  41920  limclner  41939  dvdsn1add  42231  stoweidlem14  42306  stoweidlem27  42319  stoweidlem34  42326  stoweidlem49  42341  stoweidlem56  42348  fourierdlem87  42485  iundjiun  42749  ismeannd  42756  hoidmvle  42889  prproropf1olem2  43673  perfectALTVlem2  43894  mogoldbb  43957  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  mgmhmeql  44077  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334  mndpsuppss  44426  lindslinindsimp2lem5  44524  itscnhlinecirc02p  44779