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  3067  disjiun  4010  isotr  5830  riota5f  5868  tfrexlem  6349  tfrcl  6379  nnsucuniel  6510  fopwdom  6850  dif1enen  6894  fisbth  6897  fin0  6899  fin0or  6900  diffisn  6907  finexdc  6916  fientri3  6928  unfidisj  6935  undifdc  6937  ssfirab  6947  fnfi  6950  iunfidisj  6959  dcfi  6994  ordiso2  7048  difinfinf  7114  ctmlemr  7121  exmidfodomrlemr  7215  2omotaplemap  7270  cc2lem  7279  cc3  7281  addcmpblnq  7380  mulcmpblnq  7381  ordpipqqs  7387  ltexnqq  7421  addcmpblnq0  7456  mulcmpblnq0  7457  prmu  7491  addlocpr  7549  prmuloc  7579  prmuloc2  7580  ltaddpr  7610  ltexprlemopl  7614  ltexprlemopu  7616  ltexprlemloc  7620  ltexprlemrl  7623  ltexprlemru  7625  addcanprleml  7627  addcanprlemu  7628  aptiprleml  7652  aptiprlemu  7653  ltmprr  7655  cauappcvgprlemloc  7665  archrecpr  7677  caucvgprlemloc  7688  caucvgprprlemloc  7716  caucvgprprlemexbt  7719  suplocexprlemdisj  7733  suplocexprlemloc  7734  addcmpblnr  7752  mulcmpblnrlemg  7753  mulcmpblnr  7754  ltsrprg  7760  mulgt0sr  7791  caucvgsrlemgt1  7808  suplocsrlemb  7819  axmulcl  7879  axarch  7904  axcaucvglemres  7912  axpre-suploclemres  7914  axpre-suploc  7915  readdcan  8111  cnegexlem1  8146  negeu  8162  add20  8445  apreap  8558  cru  8573  apsym  8577  apcotr  8578  apadd1  8579  apneg  8582  mulext1  8583  divdivdivap  8684  ltmul12a  8831  lemul12a  8833  lt2mul2div  8850  ledivdiv  8861  lediv12a  8865  qapne  9653  xleadd1a  9887  ixxss12  9920  ioodisj  10007  fz0fzelfz0  10141  qtri3or  10257  exbtwnzlemstep  10262  exbtwnzlemex  10264  exbtwnz  10265  rebtwn2zlemstep  10267  rebtwn2z  10269  qbtwnre  10271  btwnzge0  10314  iseqf1olemqf1o  10507  mulexpzap  10574  leexp1a  10589  expnbnd  10658  hashen  10778  fihashdom  10797  hashun  10799  zfz1iso  10835  cjap  10929  cvg1nlemres  11008  rsqrmo  11050  abs3lem  11134  cau3lem  11137  rexanre  11243  xrmaxltsup  11280  climcau  11369  sumeq2  11381  summodc  11405  fsum3cvg3  11418  fsum2d  11457  prodeq2  11579  prodmodclem2  11599  fprod2d  11645  eirrap  11799  addmodlteqALT  11879  divalglemeunn  11940  divalglemeuneg  11942  zsupcllemstep  11960  zsupssdc  11969  bezoutlemnewy  12011  bezoutlemstep  12012  bezoutlemmain  12013  bezoutlembi  12020  bezoutlemeu  12022  rpdvds  12113  isprm5lem  12155  isprm6  12161  pw2dvdslemn  12179  pw2dvdseu  12182  sqrt2irrap  12194  pythagtriplem2  12280  pythagtrip  12297  pclemub  12301  pcqmul  12317  pcexp  12323  pcneg  12338  pcprmpw2  12346  pcadd  12353  pcmpt  12355  ennnfonelemrnh  12431  ennnfonelemnn0  12437  ctinfomlemom  12442  ctiunctlemfo  12454  nninfdclemf1  12467  imasival  12745  sgrppropd  12838  ismndd  12860  mndpropd  12863  mhmeql  12898  mhmmnd  13011  issubg4m  13085  ssnmz  13103  rngpropd  13207  ringpropd  13290  islmod  13480  restbasg  13964  cnrest2  14032  cnpdis  14038  lmtopcnp  14046  txcnp  14067  txlm  14075  ismet2  14150  blininf  14220  metss2lem  14293  xmettxlem  14305  xmettx  14306  metcnp3  14307  metcnpi3  14313  addcncntoplem  14347  fsumcncntop  14352  mulcncf  14387  dedekindeulemuub  14391  dedekindeu  14397  dedekindicclemuub  14400  ivthinclemlopn  14410  ivthinclemuopn  14412  ivthinclemloc  14415  ivthinc  14417  limcimo  14430  limccnp2cntop  14442  logbgcd1irrap  14684  lgsdilem  14724  2sqlem5  14762  2sqlem9  14767  qdencn  15072  apdiff  15093