Theorem simplrr 536

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 110	. 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  3122  disjiun  4078  isotr  5946  riota5f  5987  tfrexlem  6486  tfrcl  6516  nnsucuniel  6649  pw2f1odclem  7003  fopwdom  7005  dif1enen  7050  fisbth  7053  fin0  7055  fin0or  7056  diffisn  7063  finexdc  7072  fientri3  7085  unfidisj  7092  undifdc  7094  ssfirab  7106  fnfi  7111  iunfidisj  7121  dcfi  7156  ordiso2  7210  difinfinf  7276  ctmlemr  7283  exmidfodomrlemr  7388  2omotaplemap  7451  cc2lem  7460  cc3  7462  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  ltexnqq  7603  addcmpblnq0  7638  mulcmpblnq0  7639  prmu  7673  addlocpr  7731  prmuloc  7761  prmuloc2  7762  ltaddpr  7792  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemloc  7802  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  aptiprleml  7834  aptiprlemu  7835  ltmprr  7837  cauappcvgprlemloc  7847  archrecpr  7859  caucvgprlemloc  7870  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  suplocexprlemdisj  7915  suplocexprlemloc  7916  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  ltsrprg  7942  mulgt0sr  7973  caucvgsrlemgt1  7990  suplocsrlemb  8001  axmulcl  8061  axarch  8086  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  readdcan  8294  cnegexlem1  8329  negeu  8345  add20  8629  apreap  8742  cru  8757  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  divdivdivap  8868  ltmul12a  9015  lemul12a  9017  lt2mul2div  9034  ledivdiv  9045  lediv12a  9049  qapne  9842  xleadd1a  10077  ixxss12  10110  ioodisj  10197  fz0fzelfz0  10331  zsupcllemstep  10457  zsupssdc  10466  qtri3or  10468  exbtwnzlemstep  10475  exbtwnzlemex  10477  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnre  10484  btwnzge0  10528  iseqf1olemqf1o  10736  mulexpzap  10809  leexp1a  10824  expnbnd  10893  hashen  11014  fihashdom  11033  hashun  11035  zfz1iso  11071  swrdccat  11275  reuccatpfxs1  11287  cjap  11425  cvg1nlemres  11504  rsqrmo  11546  abs3lem  11630  cau3lem  11633  rexanre  11739  xrmaxltsup  11777  climcau  11866  sumeq2  11878  summodc  11902  fsum3cvg3  11915  fsum2d  11954  prodeq2  12076  prodmodclem2  12096  fprod2d  12142  eirrap  12297  addmodlteqALT  12378  divalglemeunn  12440  divalglemeuneg  12442  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlembi  12534  bezoutlemeu  12536  rpdvds  12629  isprm5lem  12671  isprm6  12677  pw2dvdslemn  12695  pw2dvdseu  12698  sqrt2irrap  12710  pythagtriplem2  12797  pythagtrip  12814  pclemub  12818  pcqmul  12834  pcexp  12840  pcneg  12856  pcprmpw2  12864  pcadd  12871  pcmpt  12874  4sqlem13m  12934  ennnfonelemrnh  12995  ennnfonelemnn0  13001  ctinfomlemom  13006  ctiunctlemfo  13018  nninfdclemf1  13031  imasival  13347  gsumpropd2  13434  sgrppropd  13454  ismndd  13478  mndpropd  13481  mhmeql  13533  mhmmnd  13661  issubg4m  13738  ssnmz  13756  conjnmzb  13825  rngpropd  13926  ringpropd  14009  islmod  14263  psrval  14638  restbasg  14850  cnrest2  14918  cnpdis  14924  lmtopcnp  14932  txcnp  14953  txlm  14961  ismet2  15036  blininf  15106  metss2lem  15179  xmettxlem  15191  xmettx  15192  metcnp3  15193  metcnpi3  15199  addcncntoplem  15243  fsumcncntop  15249  mulcncf  15290  dedekindeulemuub  15299  dedekindeu  15305  dedekindicclemuub  15308  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthinclemloc  15323  ivthinc  15325  ivthdichlem  15333  limcimo  15347  limccnp2cntop  15359  plyf  15419  plyco  15441  plycj  15443  plyrecj  15445  dvply2g  15448  logbgcd1irrap  15652  perfectlem2  15682  lgsdilem  15714  lgsquad2lem2  15769  lgsquad3  15771  2sqlem5  15806  2sqlem9  15811  usgredg4  16021  fidcen  16379  2omap  16388  qdencn  16425  apdiff  16446