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  6610  tfrcl  6640  nnsucuniel  6773  pw2f1odclem  7140  fopwdom  7142  dif1enen  7190  fisbth  7193  fin0  7195  fin0or  7196  diffisn  7203  fidcen  7209  finexdc  7213  elssdc  7215  fientri3  7228  unfidisj  7235  undifdc  7237  ssfirab  7250  fnfi  7256  iunfidisj  7266  mapfi  7267  fissfi  7269  dcfi  7320  2omap  7324  ordiso2  7381  difinfinf  7447  ctmlemr  7454  exmidfodomrlemr  7560  2omotaplemap  7629  cc2lem  7638  cc3  7640  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  ltexnqq  7781  addcmpblnq0  7816  mulcmpblnq0  7817  prmu  7851  addlocpr  7909  prmuloc  7939  prmuloc2  7940  ltaddpr  7970  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  aptiprleml  8012  aptiprlemu  8013  ltmprr  8015  cauappcvgprlemloc  8025  archrecpr  8037  caucvgprlemloc  8048  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  suplocexprlemdisj  8093  suplocexprlemloc  8094  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  ltsrprg  8120  mulgt0sr  8151  caucvgsrlemgt1  8168  suplocsrlemb  8179  axmulcl  8239  axarch  8264  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  readdcan  8473  cnegexlem1  8508  negeu  8524  add20  8809  apreap  8923  cru  8938  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  divdivdivap  9051  ltmul12a  9198  lemul12a  9200  lt2mul2div  9217  ledivdiv  9228  lediv12a  9232  qapne  10054  xleadd1a  10291  ixxss12  10324  ioodisj  10411  fz0fzelfz0  10550  zsupcllemstep  10678  zsupssdc  10689  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnre  10707  btwnzge0  10755  iseqf1olemqf1o  10963  mulexpzap  11036  leexp1a  11051  expnbnd  11121  hashen  11244  fihashdom  11264  hashun  11266  hashf1  11308  zfz1iso  11314  swrdccat  11528  reuccatpfxs1  11540  cjap  11693  cvg1nlemres  11772  rsqrmo  11814  abs3lem  11899  cau3lem  11902  rexanre  12008  fiidxsupcl  12017  xrmaxltsup  12048  climcau  12137  sumeq2  12149  summodc  12174  fsum3cvg3  12187  fsum2d  12226  prodeq2  12348  prodmodclem2  12368  fprod2d  12414  eirrap  12569  addmodlteqALT  12650  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlembi  12806  bezoutlemeu  12808  rpdvds  12901  isprm5lem  12944  isprm6  12950  pwbdvdslemn  12968  pwbdvdseu  12971  sqrt2irrap  12984  pythagtriplem2  13073  pythagtrip  13090  pclemub  13094  pcqmul  13110  pcexp  13116  pcneg  13132  pcprmpw2  13140  pcadd  13147  pcmpt  13150  4sqlem13m  13210  ballotfilemcdc  13280  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemrnh  13364  ennnfonelemnn0  13370  ctinfomlemom  13375  ctiunctlemfo  13387  nninfdclemf1  13400  imasival  13685  sgrppropd  13786  ismndd  13808  mndpropd  13811  mhmeql  13857  mhmmnd  13977  issubg4m  14054  ssnmz  14072  conjnmzb  14141  gsumvalfi  14241  rngpropd  14360  ringpropd  14449  aprlring  14708  islmod  14735  assapropd  15122  psrval  15160  psrbaglefifi  15175  psrbagmax  15183  restbasg  15411  cnrest2  15479  cnpdis  15485  lmtopcnp  15493  txcnp  15514  txlm  15522  ismet2  15597  blininf  15667  metss2lem  15740  xmettxlem  15752  xmettx  15753  metcnp3  15754  metcnpi3  15760  addcncntoplem  15804  fsumcncntop  15810  mulcncf  15851  dedekindeulemuub  15860  dedekindeu  15866  dedekindicclemuub  15869  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthinclemloc  15884  ivthinc  15886  ivthdichlem  15894  limcimo  15908  limccnp2cntop  15920  plyf  15980  plyco  16002  plycj  16004  plyrecj  16006  dvply2g  16009  logdivlt  16141  logbgcd1irrap  16223  zprmlogbap  16235  perfectlem2  16317  lgsdilem  16368  lgsquad2lem2  16423  lgsquad3  16425  2sqlem5  16460  2sqlem9  16465  usgredg4  16678  usgr1vr  16711  subuhgr  16735  subumgr  16737  clwwlknonex2lem2  16901  eupth2lemsfi  16941  depindlem3  16971  qdencn  17295  apdiff  17321  qdiff  17322