Theorem simplrr 542

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 493	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rmob  3145  disjiun  4125  isotr  6022  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  pw2f1odclem  7134  fopwdom  7136  dif1enen  7184  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  unfidisj  7229  undifdc  7231  ssfirab  7244  fnfi  7250  iunfidisj  7260  mapfi  7261  fissfi  7263  dcfi  7315  2omap  7318  ordiso2  7375  difinfinf  7441  ctmlemr  7448  exmidfodomrlemr  7554  2omotaplemap  7623  cc2lem  7632  cc3  7634  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  ltexnqq  7775  addcmpblnq0  7810  mulcmpblnq0  7811  prmu  7845  addlocpr  7903  prmuloc  7933  prmuloc2  7934  ltaddpr  7964  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  cauappcvgprlemloc  8019  archrecpr  8031  caucvgprlemloc  8042  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemdisj  8087  suplocexprlemloc  8088  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  mulgt0sr  8145  caucvgsrlemgt1  8162  suplocsrlemb  8173  axmulcl  8233  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  readdcan  8466  cnegexlem1  8501  negeu  8517  add20  8802  apreap  8916  cru  8931  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  divdivdivap  9044  ltmul12a  9191  lemul12a  9193  lt2mul2div  9210  ledivdiv  9221  lediv12a  9225  qapne  10041  xleadd1a  10277  ixxss12  10310  ioodisj  10397  fz0fzelfz0  10536  zsupcllemstep  10664  zsupssdc  10675  qtri3or  10677  exbtwnzlemstep  10684  exbtwnzlemex  10686  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnre  10693  btwnzge0  10737  iseqf1olemqf1o  10945  mulexpzap  11018  leexp1a  11033  expnbnd  11103  hashen  11225  fihashdom  11245  hashun  11247  hashf1  11289  zfz1iso  11295  swrdccat  11509  reuccatpfxs1  11521  cjap  11674  cvg1nlemres  11753  rsqrmo  11795  abs3lem  11879  cau3lem  11882  rexanre  11988  xrmaxltsup  12026  climcau  12115  sumeq2  12127  summodc  12152  fsum3cvg3  12165  fsum2d  12204  prodeq2  12326  prodmodclem2  12346  fprod2d  12392  eirrap  12547  addmodlteqALT  12628  divalglemeunn  12690  divalglemeuneg  12692  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlembi  12784  bezoutlemeu  12786  rpdvds  12879  isprm5lem  12921  isprm6  12927  pw2dvdslemn  12945  pw2dvdseu  12948  sqrt2irrap  12960  pythagtriplem2  13047  pythagtrip  13064  pclemub  13068  pcqmul  13084  pcexp  13090  pcneg  13106  pcprmpw2  13114  pcadd  13121  pcmpt  13124  4sqlem13m  13184  ballotfilemcdc  13225  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemrnh  13309  ennnfonelemnn0  13315  ctinfomlemom  13320  ctiunctlemfo  13332  nninfdclemf1  13345  imasival  13629  sgrppropd  13730  ismndd  13752  mndpropd  13755  mhmeql  13801  mhmmnd  13921  issubg4m  13998  ssnmz  14016  conjnmzb  14085  gsumvalfi  14154  rngpropd  14256  ringpropd  14345  aprlring  14602  islmod  14629  assapropd  15016  psrval  15052  restbasg  15271  cnrest2  15339  cnpdis  15345  lmtopcnp  15353  txcnp  15374  txlm  15382  ismet2  15457  blininf  15527  metss2lem  15600  xmettxlem  15612  xmettx  15613  metcnp3  15614  metcnpi3  15620  addcncntoplem  15664  fsumcncntop  15670  mulcncf  15711  dedekindeulemuub  15720  dedekindeu  15726  dedekindicclemuub  15729  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthinclemloc  15744  ivthinc  15746  ivthdichlem  15754  limcimo  15768  limccnp2cntop  15780  plyf  15840  plyco  15862  plycj  15864  plyrecj  15866  dvply2g  15869  logdivlt  15999  logbgcd1irrap  16078  perfectlem2  16120  lgsdilem  16158  lgsquad2lem2  16213  lgsquad3  16215  2sqlem5  16250  2sqlem9  16255  usgredg4  16468  usgr1vr  16501  subuhgr  16525  subumgr  16527  clwwlknonex2lem2  16691  eupth2lemsfi  16731  depindlem3  16761  qdencn  17084  apdiff  17109  qdiff  17110