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  3082  disjiun  4029  isotr  5866  riota5f  5905  tfrexlem  6401  tfrcl  6431  nnsucuniel  6562  pw2f1odclem  6904  fopwdom  6906  dif1enen  6950  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  finexdc  6972  fientri3  6985  unfidisj  6992  undifdc  6994  ssfirab  7006  fnfi  7011  iunfidisj  7021  dcfi  7056  ordiso2  7110  difinfinf  7176  ctmlemr  7183  exmidfodomrlemr  7283  2omotaplemap  7342  cc2lem  7351  cc3  7353  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  ltexnqq  7494  addcmpblnq0  7529  mulcmpblnq0  7530  prmu  7564  addlocpr  7622  prmuloc  7652  prmuloc2  7653  ltaddpr  7683  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  aptiprleml  7725  aptiprlemu  7726  ltmprr  7728  cauappcvgprlemloc  7738  archrecpr  7750  caucvgprlemloc  7761  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  suplocexprlemdisj  7806  suplocexprlemloc  7807  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  ltsrprg  7833  mulgt0sr  7864  caucvgsrlemgt1  7881  suplocsrlemb  7892  axmulcl  7952  axarch  7977  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  readdcan  8185  cnegexlem1  8220  negeu  8236  add20  8520  apreap  8633  cru  8648  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  divdivdivap  8759  ltmul12a  8906  lemul12a  8908  lt2mul2div  8925  ledivdiv  8936  lediv12a  8940  qapne  9732  xleadd1a  9967  ixxss12  10000  ioodisj  10087  fz0fzelfz0  10221  zsupcllemstep  10338  zsupssdc  10347  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnre  10365  btwnzge0  10409  iseqf1olemqf1o  10617  mulexpzap  10690  leexp1a  10705  expnbnd  10774  hashen  10895  fihashdom  10914  hashun  10916  zfz1iso  10952  cjap  11090  cvg1nlemres  11169  rsqrmo  11211  abs3lem  11295  cau3lem  11298  rexanre  11404  xrmaxltsup  11442  climcau  11531  sumeq2  11543  summodc  11567  fsum3cvg3  11580  fsum2d  11619  prodeq2  11741  prodmodclem2  11761  fprod2d  11807  eirrap  11962  addmodlteqALT  12043  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlembi  12199  bezoutlemeu  12201  rpdvds  12294  isprm5lem  12336  isprm6  12342  pw2dvdslemn  12360  pw2dvdseu  12363  sqrt2irrap  12375  pythagtriplem2  12462  pythagtrip  12479  pclemub  12483  pcqmul  12499  pcexp  12505  pcneg  12521  pcprmpw2  12529  pcadd  12536  pcmpt  12539  4sqlem13m  12599  ennnfonelemrnh  12660  ennnfonelemnn0  12666  ctinfomlemom  12671  ctiunctlemfo  12683  nninfdclemf1  12696  imasival  13010  gsumpropd2  13097  sgrppropd  13117  ismndd  13141  mndpropd  13144  mhmeql  13196  mhmmnd  13324  issubg4m  13401  ssnmz  13419  conjnmzb  13488  rngpropd  13589  ringpropd  13672  islmod  13925  psrval  14298  restbasg  14490  cnrest2  14558  cnpdis  14564  lmtopcnp  14572  txcnp  14593  txlm  14601  ismet2  14676  blininf  14746  metss2lem  14819  xmettxlem  14831  xmettx  14832  metcnp3  14833  metcnpi3  14839  addcncntoplem  14883  fsumcncntop  14889  mulcncf  14930  dedekindeulemuub  14939  dedekindeu  14945  dedekindicclemuub  14948  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthinclemloc  14963  ivthinc  14965  ivthdichlem  14973  limcimo  14987  limccnp2cntop  14999  plyf  15059  plyco  15081  plycj  15083  plyrecj  15085  dvply2g  15088  logbgcd1irrap  15292  perfectlem2  15322  lgsdilem  15354  lgsquad2lem2  15409  lgsquad3  15411  2sqlem5  15446  2sqlem9  15451  2omap  15728  qdencn  15762  apdiff  15783