Theorem simplrr 526

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 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 481	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3038  disjiun  3971  isotr  5778  riota5f  5816  tfrexlem  6293  tfrcl  6323  nnsucuniel  6454  fopwdom  6793  dif1enen  6837  fisbth  6840  fin0  6842  fin0or  6843  diffisn  6850  finexdc  6859  fientri3  6871  unfidisj  6878  undifdc  6880  ssfirab  6890  fnfi  6893  iunfidisj  6902  dcfi  6937  ordiso2  6991  difinfinf  7057  ctmlemr  7064  exmidfodomrlemr  7149  cc2lem  7198  cc3  7200  addcmpblnq  7299  mulcmpblnq  7300  ordpipqqs  7306  ltexnqq  7340  addcmpblnq0  7375  mulcmpblnq0  7376  prmu  7410  addlocpr  7468  prmuloc  7498  prmuloc2  7499  ltaddpr  7529  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemloc  7539  ltexprlemrl  7542  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  aptiprleml  7571  aptiprlemu  7572  ltmprr  7574  cauappcvgprlemloc  7584  archrecpr  7596  caucvgprlemloc  7607  caucvgprprlemloc  7635  caucvgprprlemexbt  7638  suplocexprlemdisj  7652  suplocexprlemloc  7653  addcmpblnr  7671  mulcmpblnrlemg  7672  mulcmpblnr  7673  ltsrprg  7679  mulgt0sr  7710  caucvgsrlemgt1  7727  suplocsrlemb  7738  axmulcl  7798  axarch  7823  axcaucvglemres  7831  axpre-suploclemres  7833  axpre-suploc  7834  readdcan  8029  cnegexlem1  8064  negeu  8080  add20  8363  apreap  8476  cru  8491  apsym  8495  apcotr  8496  apadd1  8497  apneg  8500  mulext1  8501  divdivdivap  8600  ltmul12a  8746  lemul12a  8748  lt2mul2div  8765  ledivdiv  8776  lediv12a  8780  qapne  9568  xleadd1a  9800  ixxss12  9833  ioodisj  9920  fz0fzelfz0  10052  qtri3or  10168  exbtwnzlemstep  10173  exbtwnzlemex  10175  exbtwnz  10176  rebtwn2zlemstep  10178  rebtwn2z  10180  qbtwnre  10182  btwnzge0  10225  iseqf1olemqf1o  10418  mulexpzap  10485  leexp1a  10500  expnbnd  10567  hashen  10686  fihashdom  10705  hashun  10707  zfz1iso  10740  cjap  10834  cvg1nlemres  10913  rsqrmo  10955  abs3lem  11039  cau3lem  11042  rexanre  11148  xrmaxltsup  11185  climcau  11274  sumeq2  11286  summodc  11310  fsum3cvg3  11323  fsum2d  11362  prodeq2  11484  prodmodclem2  11504  fprod2d  11550  eirrap  11704  addmodlteqALT  11782  divalglemeunn  11843  divalglemeuneg  11845  zsupcllemstep  11863  zsupssdc  11872  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlembi  11923  bezoutlemeu  11925  rpdvds  12010  isprm6  12056  pw2dvdslemn  12074  pw2dvdseu  12077  sqrt2irrap  12089  pythagtriplem2  12175  pythagtrip  12192  pclemub  12196  pcqmul  12212  pcexp  12218  pcneg  12233  pcprmpw2  12241  pcadd  12248  pcmpt  12250  ennnfonelemrnh  12286  ennnfonelemnn0  12292  ctinfomlemom  12297  ctiunctlemfo  12309  nninfdclemf1  12324  restbasg  12709  cnrest2  12777  cnpdis  12783  lmtopcnp  12791  txcnp  12812  txlm  12820  ismet2  12895  blininf  12965  metss2lem  13038  xmettxlem  13050  xmettx  13051  metcnp3  13052  metcnpi3  13058  addcncntoplem  13092  fsumcncntop  13097  mulcncf  13132  dedekindeulemuub  13136  dedekindeu  13142  dedekindicclemuub  13145  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthinclemloc  13160  ivthinc  13162  limcimo  13175  limccnp2cntop  13187  logbgcd1irrap  13429  qdencn  13740  apdiff  13761