Theorem simplrr 538

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  3138  disjiun  4106  isotr  5991  riota5f  6032  tfrexlem  6567  tfrcl  6597  nnsucuniel  6730  pw2f1odclem  7089  fopwdom  7091  dif1enen  7139  fisbth  7142  fin0  7144  fin0or  7145  diffisn  7152  fidcen  7158  finexdc  7162  elssdc  7164  fientri3  7177  unfidisj  7184  undifdc  7186  ssfirab  7199  fnfi  7205  iunfidisj  7215  mapfi  7216  fissfi  7218  dcfi  7270  2omap  7271  ordiso2  7328  difinfinf  7394  ctmlemr  7401  exmidfodomrlemr  7507  2omotaplemap  7576  cc2lem  7585  cc3  7587  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  ltexnqq  7728  addcmpblnq0  7763  mulcmpblnq0  7764  prmu  7798  addlocpr  7856  prmuloc  7886  prmuloc2  7887  ltaddpr  7917  ltexprlemopl  7921  ltexprlemopu  7923  ltexprlemloc  7927  ltexprlemrl  7930  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  aptiprleml  7959  aptiprlemu  7960  ltmprr  7962  cauappcvgprlemloc  7972  archrecpr  7984  caucvgprlemloc  7995  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  suplocexprlemdisj  8040  suplocexprlemloc  8041  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  ltsrprg  8067  mulgt0sr  8098  caucvgsrlemgt1  8115  suplocsrlemb  8126  axmulcl  8186  axarch  8211  axcaucvglemres  8219  axpre-suploclemres  8221  axpre-suploc  8222  readdcan  8418  cnegexlem1  8453  negeu  8469  add20  8753  apreap  8866  cru  8881  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  divdivdivap  8992  ltmul12a  9139  lemul12a  9141  lt2mul2div  9158  ledivdiv  9169  lediv12a  9173  qapne  9977  xleadd1a  10212  ixxss12  10245  ioodisj  10332  fz0fzelfz0  10468  zsupcllemstep  10596  zsupssdc  10605  qtri3or  10607  exbtwnzlemstep  10614  exbtwnzlemex  10616  exbtwnz  10617  rebtwn2zlemstep  10619  rebtwn2z  10621  qbtwnre  10623  btwnzge0  10667  iseqf1olemqf1o  10875  mulexpzap  10948  leexp1a  10963  expnbnd  11033  hashen  11155  fihashdom  11175  hashun  11177  zfz1iso  11221  swrdccat  11435  reuccatpfxs1  11447  cjap  11599  cvg1nlemres  11678  rsqrmo  11720  abs3lem  11804  cau3lem  11807  rexanre  11913  xrmaxltsup  11951  climcau  12040  sumeq2  12052  summodc  12077  fsum3cvg3  12090  fsum2d  12129  prodeq2  12251  prodmodclem2  12271  fprod2d  12317  eirrap  12472  addmodlteqALT  12553  divalglemeunn  12615  divalglemeuneg  12617  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemmain  12702  bezoutlembi  12709  bezoutlemeu  12711  rpdvds  12804  isprm5lem  12846  isprm6  12852  pw2dvdslemn  12870  pw2dvdseu  12873  sqrt2irrap  12885  pythagtriplem2  12972  pythagtrip  12989  pclemub  12993  pcqmul  13009  pcexp  13015  pcneg  13031  pcprmpw2  13039  pcadd  13046  pcmpt  13049  4sqlem13m  13109  ballotfilemcdc  13150  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemrnh  13188  ennnfonelemnn0  13194  ctinfomlemom  13199  ctiunctlemfo  13211  nninfdclemf1  13224  imasival  13540  gsumpropd2  13627  sgrppropd  13647  ismndd  13671  mndpropd  13674  mhmeql  13726  mhmmnd  13854  issubg4m  13931  ssnmz  13949  conjnmzb  14018  rngpropd  14120  ringpropd  14203  aprlring  14460  islmod  14488  psrval  14863  restbasg  15082  cnrest2  15150  cnpdis  15156  lmtopcnp  15164  txcnp  15185  txlm  15193  ismet2  15268  blininf  15338  metss2lem  15411  xmettxlem  15423  xmettx  15424  metcnp3  15425  metcnpi3  15431  addcncntoplem  15475  fsumcncntop  15481  mulcncf  15522  dedekindeulemuub  15531  dedekindeu  15537  dedekindicclemuub  15540  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthinclemloc  15555  ivthinc  15557  ivthdichlem  15565  limcimo  15579  limccnp2cntop  15591  plyf  15651  plyco  15673  plycj  15675  plyrecj  15677  dvply2g  15680  logbgcd1irrap  15884  perfectlem2  15917  lgsdilem  15949  lgsquad2lem2  16004  lgsquad3  16006  2sqlem5  16041  2sqlem9  16046  usgredg4  16259  usgr1vr  16292  subuhgr  16316  subumgr  16318  clwwlknonex2lem2  16482  eupth2lemsfi  16522  depindlem3  16552  qdencn  16856  apdiff  16881  qdiff  16882  trimul0or  16894  gfsumval  16911