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  3082  disjiun  4029  f1imass  5824  riota5f  5905  tfrexlem  6401  tfrcl  6431  nnsucuniel  6562  nntr2  6570  pw2f1odclem  6904  fopwdom  6906  fidceq  6939  fisbth  6953  fientri3  6985  unsnfidcex  6990  undifdc  6994  iunfidisj  7021  fiuni  7053  ordiso2  7110  nninfninc  7198  acfun  7292  2omotaplemap  7342  ccfunen  7349  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  addcmpblnq0  7529  mulcmpblnq0  7530  prml  7563  addlocpr  7622  prmuloc  7652  mullocpr  7657  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  aptiprleml  7725  ltmprr  7728  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemloc  7738  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemloc  7761  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  suplocexprlemrl  7803  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  ltsrprg  7833  mulgt0sr  7864  caucvgsrlemgt1  7881  suplocsrlemb  7892  axmulcl  7952  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  cnegexlem1  8220  negeu  8236  add20  8520  apreap  8633  cru  8648  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulge0  8665  mulap0  8700  divdivdivap  8759  prodgt0  8898  ltmul12a  8906  lt2mul2div  8925  ledivdiv  8936  lediv12a  8940  qapne  9732  xleadd1a  9967  ixxss12  10000  elfz0ubfz0  10219  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  btwnzge0  10409  iseqf1olemqf1o  10617  mulexpzap  10690  leexp1a  10705  hashen  10895  fihashdom  10914  hashun  10916  cjap  11090  cvg1nlemres  11169  rsqrmo  11211  abslt  11272  abs3lem  11295  cau3lem  11298  rexanre  11404  xrmaxltsup  11442  climcau  11531  sumeq2  11543  summodc  11567  fisumss  11576  fsum2d  11619  fsumabs  11649  fsumiun  11661  prodeq2  11741  prodmodclem2  11761  fprodcl2lem  11789  fprodap0  11805  fprod2d  11807  fprodrec  11813  fprodap0f  11820  fprodle  11824  eirrap  11962  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlembi  12199  bezoutlemeu  12201  qredeu  12292  isprm5lem  12336  pw2dvdseu  12363  sqrt2irrap  12375  pythagtriplem2  12462  pythagtrip  12479  pclemub  12483  pcqmul  12499  pcexp  12505  pcneg  12521  pcprmpw2  12529  pcadd  12536  prmpwdvds  12551  4sqlem13m  12599  ennnfonelemg  12647  ennnfonelemrnh  12660  ctiunctlemfo  12683  nninfdclemf1  12696  imasival  13010  sgrppropd  13117  ismndd  13141  mndpropd  13144  mhmeql  13196  mhmmnd  13324  mulgfng  13332  issubg4m  13401  ssnmz  13419  conjnmzb  13488  rngpropd  13589  ringpropd  13672  dvdsrtr  13735  islmod  13925  mplsubgfilemcl  14333  restbasg  14512  cnpnei  14563  cnptoprest2  14584  cnpdis  14586  lmtopcnp  14594  txcnp  14615  ismet2  14698  blininf  14768  metss2lem  14841  xmettxlem  14853  xmettx  14854  metcnp  14856  metcnpi3  14861  addcncntoplem  14905  fsumcncntop  14911  mulc1cncf  14933  cncfco  14935  mulcncf  14952  dedekindeulemuub  14961  dedekindeu  14967  dedekindicclemuub  14970  ivthinclemloc  14985  ivthinc  14987  limcimo  15009  limccnp2cntop  15021  dveflem  15070  plyf  15081  plyco  15103  plycj  15105  dvply2g  15110  logbgcd1irrap  15314  perfectlem2  15344  lgsdilem  15376  lgsquad2lem2  15431  lgsquad3  15433  2sqlem5  15468  2sqlem9  15473  2omap  15750  qdencn  15784  apdiff  15805