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  3102  disjiun  4057  f1imass  5871  riota5f  5954  tfrexlem  6450  tfrcl  6480  nnsucuniel  6611  nntr2  6619  pw2f1odclem  6963  fopwdom  6965  fidceq  6999  fisbth  7013  fientri3  7045  unsnfidcex  7050  undifdc  7054  iunfidisj  7081  fiuni  7113  ordiso2  7170  nninfninc  7258  acfun  7357  2omotaplemap  7411  ccfunen  7418  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  addcmpblnq0  7598  mulcmpblnq0  7599  prml  7632  addlocpr  7691  prmuloc  7721  mullocpr  7726  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemloc  7762  ltexprlemrl  7765  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  aptiprleml  7794  ltmprr  7797  cauappcvgprlemopl  7801  cauappcvgprlemopu  7803  cauappcvgprlemloc  7807  caucvgprlemopl  7824  caucvgprlemopu  7826  caucvgprlemloc  7830  caucvgprprlemopu  7854  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  caucvgprprlemaddq  7863  suplocexprlemrl  7872  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  ltsrprg  7902  mulgt0sr  7933  caucvgsrlemgt1  7950  suplocsrlemb  7961  axmulcl  8021  axcaucvglemres  8054  axpre-suploclemres  8056  axpre-suploc  8057  cnegexlem1  8289  negeu  8305  add20  8589  apreap  8702  cru  8717  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  mulge0  8734  mulap0  8769  divdivdivap  8828  prodgt0  8967  ltmul12a  8975  lt2mul2div  8994  ledivdiv  9005  lediv12a  9009  qapne  9802  xleadd1a  10037  ixxss12  10070  elfz0ubfz0  10289  qtri3or  10427  exbtwnzlemstep  10434  exbtwnzlemex  10436  exbtwnz  10437  rebtwn2zlemstep  10439  rebtwn2z  10441  btwnzge0  10487  iseqf1olemqf1o  10695  mulexpzap  10768  leexp1a  10783  hashen  10973  fihashdom  10992  hashun  10994  swrdccatin1  11223  pfxccatin12lem3  11230  pfxccat3  11232  cjap  11383  cvg1nlemres  11462  rsqrmo  11504  abslt  11565  abs3lem  11588  cau3lem  11591  rexanre  11697  xrmaxltsup  11735  climcau  11824  sumeq2  11836  summodc  11860  fisumss  11869  fsum2d  11912  fsumabs  11942  fsumiun  11954  prodeq2  12034  prodmodclem2  12054  fprodcl2lem  12082  fprodap0  12098  fprod2d  12100  fprodrec  12106  fprodap0f  12113  fprodle  12117  eirrap  12255  divalglemeunn  12398  divalglemeuneg  12400  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlembi  12492  bezoutlemeu  12494  qredeu  12585  isprm5lem  12629  pw2dvdseu  12656  sqrt2irrap  12668  pythagtriplem2  12755  pythagtrip  12772  pclemub  12776  pcqmul  12792  pcexp  12798  pcneg  12814  pcprmpw2  12822  pcadd  12829  prmpwdvds  12844  4sqlem13m  12892  ennnfonelemg  12940  ennnfonelemrnh  12953  ctiunctlemfo  12976  nninfdclemf1  12989  imasival  13305  sgrppropd  13412  ismndd  13436  mndpropd  13439  mhmeql  13491  mhmmnd  13619  mulgfng  13627  issubg4m  13696  ssnmz  13714  conjnmzb  13783  rngpropd  13884  ringpropd  13967  dvdsrtr  14030  islmod  14220  mplsubgfilemcl  14628  restbasg  14807  cnpnei  14858  cnptoprest2  14879  cnpdis  14881  lmtopcnp  14889  txcnp  14910  ismet2  14993  blininf  15063  metss2lem  15136  xmettxlem  15148  xmettx  15149  metcnp  15151  metcnpi3  15156  addcncntoplem  15200  fsumcncntop  15206  mulc1cncf  15228  cncfco  15230  mulcncf  15247  dedekindeulemuub  15256  dedekindeu  15262  dedekindicclemuub  15265  ivthinclemloc  15280  ivthinc  15282  limcimo  15304  limccnp2cntop  15316  dveflem  15365  plyf  15376  plyco  15398  plycj  15400  dvply2g  15405  logbgcd1irrap  15609  perfectlem2  15639  lgsdilem  15671  lgsquad2lem2  15726  lgsquad3  15728  2sqlem5  15763  2sqlem9  15768  usgredg4  15978  2omap  16270  pw1map  16272  qdencn  16306  apdiff  16327