Theorem simplrl 537

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  3125  disjiun  4083  f1imass  5915  riota5f  5998  tfrexlem  6500  tfrcl  6530  nnsucuniel  6663  nntr2  6671  pw2f1odclem  7020  fopwdom  7022  fidceq  7056  fisbth  7072  fidcen  7088  fientri3  7107  unsnfidcex  7112  undifdc  7116  iunfidisj  7145  fiuni  7177  ordiso2  7234  nninfninc  7322  acfun  7422  2omotaplemap  7476  ccfunen  7483  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  addcmpblnq0  7663  mulcmpblnq0  7664  prml  7697  addlocpr  7756  prmuloc  7786  mullocpr  7791  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  ltmprr  7862  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemloc  7872  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemloc  7895  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  suplocexprlemrl  7937  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  mulgt0sr  7998  caucvgsrlemgt1  8015  suplocsrlemb  8026  axmulcl  8086  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  cnegexlem1  8354  negeu  8370  add20  8654  apreap  8767  cru  8782  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulge0  8799  mulap0  8834  divdivdivap  8893  prodgt0  9032  ltmul12a  9040  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  qapne  9873  xleadd1a  10108  ixxss12  10141  elfz0ubfz0  10360  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  btwnzge0  10561  iseqf1olemqf1o  10769  mulexpzap  10842  leexp1a  10857  hashen  11047  fihashdom  11067  hashun  11069  swrdccatin1  11307  pfxccatin12lem3  11314  pfxccat3  11316  cjap  11468  cvg1nlemres  11547  rsqrmo  11589  abslt  11650  abs3lem  11673  cau3lem  11676  rexanre  11782  xrmaxltsup  11820  climcau  11909  sumeq2  11921  summodc  11946  fisumss  11955  fsum2d  11998  fsumabs  12028  fsumiun  12040  prodeq2  12120  prodmodclem2  12140  fprodcl2lem  12168  fprodap0  12184  fprod2d  12186  fprodrec  12192  fprodap0f  12199  fprodle  12203  eirrap  12341  divalglemeunn  12484  divalglemeuneg  12486  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlembi  12578  bezoutlemeu  12580  qredeu  12671  isprm5lem  12715  pw2dvdseu  12742  sqrt2irrap  12754  pythagtriplem2  12841  pythagtrip  12858  pclemub  12862  pcqmul  12878  pcexp  12884  pcneg  12900  pcprmpw2  12908  pcadd  12915  prmpwdvds  12930  4sqlem13m  12978  ennnfonelemg  13026  ennnfonelemrnh  13039  ctiunctlemfo  13062  nninfdclemf1  13075  imasival  13391  sgrppropd  13498  ismndd  13522  mndpropd  13525  mhmeql  13577  mhmmnd  13705  mulgfng  13713  issubg4m  13782  ssnmz  13800  conjnmzb  13869  rngpropd  13971  ringpropd  14054  dvdsrtr  14118  islmod  14308  mplsubgfilemcl  14716  restbasg  14895  cnpnei  14946  cnptoprest2  14967  cnpdis  14969  lmtopcnp  14977  txcnp  14998  ismet2  15081  blininf  15151  metss2lem  15224  xmettxlem  15236  xmettx  15237  metcnp  15239  metcnpi3  15244  addcncntoplem  15288  fsumcncntop  15294  mulc1cncf  15316  cncfco  15318  mulcncf  15335  dedekindeulemuub  15344  dedekindeu  15350  dedekindicclemuub  15353  ivthinclemloc  15368  ivthinc  15370  limcimo  15392  limccnp2cntop  15404  dveflem  15453  plyf  15464  plyco  15486  plycj  15488  dvply2g  15493  logbgcd1irrap  15697  perfectlem2  15727  lgsdilem  15759  lgsquad2lem2  15814  lgsquad3  15816  2sqlem5  15851  2sqlem9  15856  usgredg4  16069  usgr1eop  16099  usgr1vr  16102  subuhgr  16126  subumgr  16128  subusgr  16129  clwwlknonex2lem2  16292  2omap  16615  pw1map  16617  qdencn  16652  apdiff  16673  gfsumval  16701