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  6025  riota5f  6068  tfrexlem  6609  tfrcl  6639  nnsucuniel  6772  pw2f1odclem  7139  fopwdom  7141  dif1enen  7189  fisbth  7192  fin0  7194  fin0or  7195  diffisn  7202  fidcen  7208  finexdc  7212  elssdc  7214  fientri3  7227  unfidisj  7234  undifdc  7236  ssfirab  7249  fnfi  7255  iunfidisj  7265  mapfi  7266  fissfi  7268  dcfi  7321  2omap  7325  ordiso2  7382  difinfinf  7448  ctmlemr  7455  exmidfodomrlemr  7561  2omotaplemap  7630  cc2lem  7639  cc3  7641  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  ltexnqq  7782  addcmpblnq0  7817  mulcmpblnq0  7818  prmu  7852  addlocpr  7910  prmuloc  7940  prmuloc2  7941  ltaddpr  7971  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemloc  7981  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  aptiprleml  8013  aptiprlemu  8014  ltmprr  8016  cauappcvgprlemloc  8026  archrecpr  8038  caucvgprlemloc  8049  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  suplocexprlemdisj  8094  suplocexprlemloc  8095  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  ltsrprg  8121  mulgt0sr  8152  caucvgsrlemgt1  8169  suplocsrlemb  8180  axmulcl  8240  axarch  8265  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  readdcan  8474  cnegexlem1  8509  negeu  8525  add20  8810  apreap  8924  cru  8939  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  divdivdivap  9052  ltmul12a  9199  lemul12a  9201  lt2mul2div  9218  ledivdiv  9229  lediv12a  9233  qapne  10056  xleadd1a  10293  ixxss12  10326  ioodisj  10413  fz0fzelfz0  10552  zsupcllemstep  10680  zsupssdc  10691  qtri3or  10693  exbtwnzlemstep  10700  exbtwnzlemex  10702  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2z  10707  qbtwnre  10709  btwnzge0  10757  iseqf1olemqf1o  10965  mulexpzap  11038  leexp1a  11053  expnbnd  11123  hashen  11246  fihashdom  11266  hashun  11268  hashf1  11310  zfz1iso  11316  swrdccat  11530  reuccatpfxs1  11542  cjap  11695  cvg1nlemres  11774  rsqrmo  11816  abs3lem  11901  cau3lem  11904  rexanre  12010  fiidxsupcl  12019  xrmaxltsup  12050  climcau  12139  sumeq2  12151  summodc  12176  fsum3cvg3  12189  fsum2d  12228  prodeq2  12350  prodmodclem2  12370  fprod2d  12416  eirrap  12571  addmodlteqALT  12652  divalglemeunn  12714  divalglemeuneg  12716  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlembi  12808  bezoutlemeu  12810  rpdvds  12903  isprm5lem  12946  isprm6  12952  pwbdvdslemn  12970  pwbdvdseu  12973  sqrt2irrap  12986  pythagtriplem2  13075  pythagtrip  13092  pclemub  13096  pcqmul  13112  pcexp  13118  pcneg  13134  pcprmpw2  13142  pcadd  13149  pcmpt  13152  4sqlem13m  13212  ballotfilemcdc  13282  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemrnh  13366  ennnfonelemnn0  13372  ctinfomlemom  13377  ctiunctlemfo  13389  nninfdclemf1  13402  imasival  13687  sgrppropd  13788  ismndd  13810  mndpropd  13813  mhmeql  13859  mhmmnd  13979  issubg4m  14056  ssnmz  14074  conjnmzb  14143  gsumvalfi  14243  rngpropd  14362  ringpropd  14451  aprlring  14710  islmod  14737  assapropd  15124  psrval  15162  psrbaglefifi  15177  restbasg  15406  cnrest2  15474  cnpdis  15480  lmtopcnp  15488  txcnp  15509  txlm  15517  ismet2  15592  blininf  15662  metss2lem  15735  xmettxlem  15747  xmettx  15748  metcnp3  15749  metcnpi3  15755  addcncntoplem  15799  fsumcncntop  15805  mulcncf  15846  dedekindeulemuub  15855  dedekindeu  15861  dedekindicclemuub  15864  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthinclemloc  15879  ivthinc  15881  ivthdichlem  15889  limcimo  15903  limccnp2cntop  15915  plyf  15975  plyco  15997  plycj  15999  plyrecj  16001  dvply2g  16004  logdivlt  16136  logbgcd1irrap  16218  zprmlogbap  16230  perfectlem2  16312  lgsdilem  16363  lgsquad2lem2  16418  lgsquad3  16420  2sqlem5  16455  2sqlem9  16460  usgredg4  16673  usgr1vr  16706  subuhgr  16730  subumgr  16732  clwwlknonex2lem2  16896  eupth2lemsfi  16936  depindlem3  16966  qdencn  17290  apdiff  17316  qdiff  17317