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  8467  cnegexlem1  8502  negeu  8518  add20  8803  apreap  8917  cru  8932  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  divdivdivap  9045  ltmul12a  9192  lemul12a  9194  lt2mul2div  9211  ledivdiv  9222  lediv12a  9226  qapne  10048  xleadd1a  10285  ixxss12  10318  ioodisj  10405  fz0fzelfz0  10544  zsupcllemstep  10672  zsupssdc  10683  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnre  10701  btwnzge0  10748  iseqf1olemqf1o  10956  mulexpzap  11029  leexp1a  11044  expnbnd  11114  hashen  11237  fihashdom  11257  hashun  11259  hashf1  11301  zfz1iso  11307  swrdccat  11521  reuccatpfxs1  11533  cjap  11686  cvg1nlemres  11765  rsqrmo  11807  abs3lem  11892  cau3lem  11895  rexanre  12001  xrmaxltsup  12040  climcau  12129  sumeq2  12141  summodc  12166  fsum3cvg3  12179  fsum2d  12218  prodeq2  12340  prodmodclem2  12360  fprod2d  12406  eirrap  12561  addmodlteqALT  12642  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlembi  12798  bezoutlemeu  12800  rpdvds  12893  isprm5lem  12936  isprm6  12942  pwbdvdslemn  12960  pwbdvdseu  12963  sqrt2irrap  12976  pythagtriplem2  13065  pythagtrip  13082  pclemub  13086  pcqmul  13102  pcexp  13108  pcneg  13124  pcprmpw2  13132  pcadd  13139  pcmpt  13142  4sqlem13m  13202  ballotfilemcdc  13272  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemrnh  13356  ennnfonelemnn0  13362  ctinfomlemom  13367  ctiunctlemfo  13379  nninfdclemf1  13392  imasival  13676  sgrppropd  13777  ismndd  13799  mndpropd  13802  mhmeql  13848  mhmmnd  13968  issubg4m  14045  ssnmz  14063  conjnmzb  14132  gsumvalfi  14201  rngpropd  14303  ringpropd  14392  aprlring  14649  islmod  14676  assapropd  15063  psrval  15099  restbasg  15318  cnrest2  15386  cnpdis  15392  lmtopcnp  15400  txcnp  15421  txlm  15429  ismet2  15504  blininf  15574  metss2lem  15647  xmettxlem  15659  xmettx  15660  metcnp3  15661  metcnpi3  15667  addcncntoplem  15711  fsumcncntop  15717  mulcncf  15758  dedekindeulemuub  15767  dedekindeu  15773  dedekindicclemuub  15776  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthinclemloc  15791  ivthinc  15793  ivthdichlem  15801  limcimo  15815  limccnp2cntop  15827  plyf  15887  plyco  15909  plycj  15911  plyrecj  15913  dvply2g  15916  logdivlt  16046  logbgcd1irrap  16125  zprmlogbap  16137  perfectlem2  16219  lgsdilem  16265  lgsquad2lem2  16320  lgsquad3  16322  2sqlem5  16357  2sqlem9  16362  usgredg4  16575  usgr1vr  16608  subuhgr  16632  subumgr  16634  clwwlknonex2lem2  16798  eupth2lemsfi  16838  depindlem3  16868  qdencn  17191  apdiff  17216  qdiff  17217