Theorem simplrl 535

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3123  disjiun  4081  f1imass  5910  riota5f  5993  tfrexlem  6495  tfrcl  6525  nnsucuniel  6658  nntr2  6666  pw2f1odclem  7015  fopwdom  7017  fidceq  7051  fisbth  7067  fidcen  7083  fientri3  7102  unsnfidcex  7107  undifdc  7111  iunfidisj  7139  fiuni  7171  ordiso2  7228  nninfninc  7316  acfun  7415  2omotaplemap  7469  ccfunen  7476  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  addcmpblnq0  7656  mulcmpblnq0  7657  prml  7690  addlocpr  7749  prmuloc  7779  mullocpr  7784  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemloc  7820  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  aptiprleml  7852  ltmprr  7855  cauappcvgprlemopl  7859  cauappcvgprlemopu  7861  cauappcvgprlemloc  7865  caucvgprlemopl  7882  caucvgprlemopu  7884  caucvgprlemloc  7888  caucvgprprlemopu  7912  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  caucvgprprlemaddq  7921  suplocexprlemrl  7930  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemub  7936  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  ltsrprg  7960  mulgt0sr  7991  caucvgsrlemgt1  8008  suplocsrlemb  8019  axmulcl  8079  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  cnegexlem1  8347  negeu  8363  add20  8647  apreap  8760  cru  8775  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  mulge0  8792  mulap0  8827  divdivdivap  8886  prodgt0  9025  ltmul12a  9033  lt2mul2div  9052  ledivdiv  9063  lediv12a  9067  qapne  9866  xleadd1a  10101  ixxss12  10134  elfz0ubfz0  10353  qtri3or  10493  exbtwnzlemstep  10500  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  btwnzge0  10553  iseqf1olemqf1o  10761  mulexpzap  10834  leexp1a  10849  hashen  11039  fihashdom  11059  hashun  11061  swrdccatin1  11299  pfxccatin12lem3  11306  pfxccat3  11308  cjap  11460  cvg1nlemres  11539  rsqrmo  11581  abslt  11642  abs3lem  11665  cau3lem  11668  rexanre  11774  xrmaxltsup  11812  climcau  11901  sumeq2  11913  summodc  11937  fisumss  11946  fsum2d  11989  fsumabs  12019  fsumiun  12031  prodeq2  12111  prodmodclem2  12131  fprodcl2lem  12159  fprodap0  12175  fprod2d  12177  fprodrec  12183  fprodap0f  12190  fprodle  12194  eirrap  12332  divalglemeunn  12475  divalglemeuneg  12477  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlembi  12569  bezoutlemeu  12571  qredeu  12662  isprm5lem  12706  pw2dvdseu  12733  sqrt2irrap  12745  pythagtriplem2  12832  pythagtrip  12849  pclemub  12853  pcqmul  12869  pcexp  12875  pcneg  12891  pcprmpw2  12899  pcadd  12906  prmpwdvds  12921  4sqlem13m  12969  ennnfonelemg  13017  ennnfonelemrnh  13030  ctiunctlemfo  13053  nninfdclemf1  13066  imasival  13382  sgrppropd  13489  ismndd  13513  mndpropd  13516  mhmeql  13568  mhmmnd  13696  mulgfng  13704  issubg4m  13773  ssnmz  13791  conjnmzb  13860  rngpropd  13961  ringpropd  14044  dvdsrtr  14108  islmod  14298  mplsubgfilemcl  14706  restbasg  14885  cnpnei  14936  cnptoprest2  14957  cnpdis  14959  lmtopcnp  14967  txcnp  14988  ismet2  15071  blininf  15141  metss2lem  15214  xmettxlem  15226  xmettx  15227  metcnp  15229  metcnpi3  15234  addcncntoplem  15278  fsumcncntop  15284  mulc1cncf  15306  cncfco  15308  mulcncf  15325  dedekindeulemuub  15334  dedekindeu  15340  dedekindicclemuub  15343  ivthinclemloc  15358  ivthinc  15360  limcimo  15382  limccnp2cntop  15394  dveflem  15443  plyf  15454  plyco  15476  plycj  15478  dvply2g  15483  logbgcd1irrap  15687  perfectlem2  15717  lgsdilem  15749  lgsquad2lem2  15804  lgsquad3  15806  2sqlem5  15841  2sqlem9  15846  usgredg4  16059  usgr1eop  16089  usgr1vr  16092  clwwlknonex2lem2  16247  2omap  16544  pw1map  16546  qdencn  16581  apdiff  16602  gfsumval  16630