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  3138  disjiun  4106  f1imass  5949  riota5f  6032  tfrexlem  6567  tfrcl  6597  nnsucuniel  6730  nntr2  6738  pw2f1odclem  7089  fopwdom  7091  fidceq  7126  fisbth  7142  fidcen  7158  fientri3  7177  unsnfidcex  7182  undifdc  7186  iunfidisj  7215  fiuni  7267  2omap  7271  ordiso2  7328  nninfninc  7416  acfun  7516  2omotaplemap  7576  ccfunen  7583  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  addcmpblnq0  7763  mulcmpblnq0  7764  prml  7797  addlocpr  7856  prmuloc  7886  mullocpr  7891  ltexprlemopl  7921  ltexprlemopu  7923  ltexprlemloc  7927  ltexprlemrl  7930  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  aptiprleml  7959  ltmprr  7962  cauappcvgprlemopl  7966  cauappcvgprlemopu  7968  cauappcvgprlemloc  7972  caucvgprlemopl  7989  caucvgprlemopu  7991  caucvgprlemloc  7995  caucvgprprlemopu  8019  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  caucvgprprlemaddq  8028  suplocexprlemrl  8037  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemub  8043  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  ltsrprg  8067  mulgt0sr  8098  caucvgsrlemgt1  8115  suplocsrlemb  8126  axmulcl  8186  axcaucvglemres  8219  axpre-suploclemres  8221  axpre-suploc  8222  cnegexlem1  8453  negeu  8469  add20  8753  apreap  8866  cru  8881  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  mulge0  8898  mulap0  8933  divdivdivap  8992  prodgt0  9131  ltmul12a  9139  lt2mul2div  9158  ledivdiv  9169  lediv12a  9173  qapne  9977  xleadd1a  10212  ixxss12  10245  elfz0ubfz0  10466  qtri3or  10607  exbtwnzlemstep  10614  exbtwnzlemex  10616  exbtwnz  10617  rebtwn2zlemstep  10619  rebtwn2z  10621  btwnzge0  10667  iseqf1olemqf1o  10875  mulexpzap  10948  leexp1a  10963  hashen  11155  fihashdom  11175  hashun  11177  swrdccatin1  11425  pfxccatin12lem3  11432  pfxccat3  11434  cjap  11599  cvg1nlemres  11678  rsqrmo  11720  abslt  11781  abs3lem  11804  cau3lem  11807  rexanre  11913  xrmaxltsup  11951  climcau  12040  sumeq2  12052  summodc  12077  fisumss  12086  fsum2d  12129  fsumabs  12159  fsumiun  12171  prodeq2  12251  prodmodclem2  12271  fprodcl2lem  12299  fprodap0  12315  fprod2d  12317  fprodrec  12323  fprodap0f  12330  fprodle  12334  eirrap  12472  divalglemeunn  12615  divalglemeuneg  12617  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemmain  12702  bezoutlembi  12709  bezoutlemeu  12711  qredeu  12802  isprm5lem  12846  pw2dvdseu  12873  sqrt2irrap  12885  pythagtriplem2  12972  pythagtrip  12989  pclemub  12993  pcqmul  13009  pcexp  13015  pcneg  13031  pcprmpw2  13039  pcadd  13046  prmpwdvds  13061  4sqlem13m  13109  ennnfonelemg  13175  ennnfonelemrnh  13188  ctiunctlemfo  13211  nninfdclemf1  13224  imasival  13540  sgrppropd  13647  ismndd  13671  mndpropd  13674  mhmeql  13726  mhmmnd  13854  mulgfng  13862  issubg4m  13931  ssnmz  13949  conjnmzb  14018  rngpropd  14120  ringpropd  14203  dvdsrtr  14268  aprlring  14460  islmod  14488  mplsubgfilemcl  14903  restbasg  15082  cnpnei  15133  cnptoprest2  15154  cnpdis  15156  lmtopcnp  15164  txcnp  15185  ismet2  15268  blininf  15338  metss2lem  15411  xmettxlem  15423  xmettx  15424  metcnp  15426  metcnpi3  15431  addcncntoplem  15475  fsumcncntop  15481  mulc1cncf  15503  cncfco  15505  mulcncf  15522  dedekindeulemuub  15531  dedekindeu  15537  dedekindicclemuub  15540  ivthinclemloc  15555  ivthinc  15557  limcimo  15579  limccnp2cntop  15591  dveflem  15640  plyf  15651  plyco  15673  plycj  15675  dvply2g  15680  logbgcd1irrap  15884  perfectlem2  15917  lgsdilem  15949  lgsquad2lem2  16004  lgsquad3  16006  2sqlem5  16041  2sqlem9  16046  usgredg4  16259  usgr1eop  16289  usgr1vr  16292  subuhgr  16316  subumgr  16318  subusgr  16319  clwwlknonex2lem2  16482  pw1map  16818  qdencn  16856  apdiff  16881  qdiff  16882  gfsumval  16911