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

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  3145  disjiun  4123  isotr  6016  riota5f  6059  tfrexlem  6599  tfrcl  6629  nnsucuniel  6762  pw2f1odclem  7128  fopwdom  7130  dif1enen  7178  fisbth  7181  fin0  7183  fin0or  7184  diffisn  7191  fidcen  7197  finexdc  7201  elssdc  7203  fientri3  7216  unfidisj  7223  undifdc  7225  ssfirab  7238  fnfi  7244  iunfidisj  7254  mapfi  7255  fissfi  7257  dcfi  7309  2omap  7312  ordiso2  7369  difinfinf  7435  ctmlemr  7442  exmidfodomrlemr  7548  2omotaplemap  7617  cc2lem  7626  cc3  7628  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  ltexnqq  7769  addcmpblnq0  7804  mulcmpblnq0  7805  prmu  7839  addlocpr  7897  prmuloc  7927  prmuloc2  7928  ltaddpr  7958  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemloc  7968  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  aptiprleml  8000  aptiprlemu  8001  ltmprr  8003  cauappcvgprlemloc  8013  archrecpr  8025  caucvgprlemloc  8036  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  suplocexprlemdisj  8081  suplocexprlemloc  8082  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  ltsrprg  8108  mulgt0sr  8139  caucvgsrlemgt1  8156  suplocsrlemb  8167  axmulcl  8227  axarch  8252  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  readdcan  8460  cnegexlem1  8495  negeu  8511  add20  8796  apreap  8909  cru  8924  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  divdivdivap  9037  ltmul12a  9184  lemul12a  9186  lt2mul2div  9203  ledivdiv  9214  lediv12a  9218  qapne  10022  xleadd1a  10258  ixxss12  10291  ioodisj  10378  fz0fzelfz0  10517  zsupcllemstep  10645  zsupssdc  10656  qtri3or  10658  exbtwnzlemstep  10665  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnre  10674  btwnzge0  10718  iseqf1olemqf1o  10926  mulexpzap  10999  leexp1a  11014  expnbnd  11084  hashen  11206  fihashdom  11226  hashun  11228  hashf1  11270  zfz1iso  11276  swrdccat  11490  reuccatpfxs1  11502  cjap  11655  cvg1nlemres  11734  rsqrmo  11776  abs3lem  11860  cau3lem  11863  rexanre  11969  xrmaxltsup  12007  climcau  12096  sumeq2  12108  summodc  12133  fsum3cvg3  12146  fsum2d  12185  prodeq2  12307  prodmodclem2  12327  fprod2d  12373  eirrap  12528  addmodlteqALT  12609  divalglemeunn  12671  divalglemeuneg  12673  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlembi  12765  bezoutlemeu  12767  rpdvds  12860  isprm5lem  12902  isprm6  12908  pw2dvdslemn  12926  pw2dvdseu  12929  sqrt2irrap  12941  pythagtriplem2  13028  pythagtrip  13045  pclemub  13049  pcqmul  13065  pcexp  13071  pcneg  13087  pcprmpw2  13095  pcadd  13102  pcmpt  13105  4sqlem13m  13165  ballotfilemcdc  13206  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemrnh  13290  ennnfonelemnn0  13296  ctinfomlemom  13301  ctiunctlemfo  13313  nninfdclemf1  13326  imasival  13610  sgrppropd  13711  ismndd  13733  mndpropd  13736  mhmeql  13782  mhmmnd  13902  issubg4m  13979  ssnmz  13997  conjnmzb  14066  gsumvalfi  14135  rngpropd  14237  ringpropd  14326  aprlring  14583  islmod  14610  assapropd  14997  psrval  15033  restbasg  15252  cnrest2  15320  cnpdis  15326  lmtopcnp  15334  txcnp  15355  txlm  15363  ismet2  15438  blininf  15508  metss2lem  15581  xmettxlem  15593  xmettx  15594  metcnp3  15595  metcnpi3  15601  addcncntoplem  15645  fsumcncntop  15651  mulcncf  15692  dedekindeulemuub  15701  dedekindeu  15707  dedekindicclemuub  15710  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthinclemloc  15725  ivthinc  15727  ivthdichlem  15735  limcimo  15749  limccnp2cntop  15761  plyf  15821  plyco  15843  plycj  15845  plyrecj  15847  dvply2g  15850  logbgcd1irrap  16055  perfectlem2  16097  lgsdilem  16129  lgsquad2lem2  16184  lgsquad3  16186  2sqlem5  16221  2sqlem9  16226  usgredg4  16439  usgr1vr  16472  subuhgr  16496  subumgr  16498  clwwlknonex2lem2  16662  eupth2lemsfi  16702  depindlem3  16732  qdencn  17046  apdiff  17071  qdiff  17072