Theorem simpllr 540

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simpllr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 492	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:  simp-4r  548  f1o2ndf1  6458  tfrlem1  6573  tfr1onlemaccex  6613  tfrcllemaccex  6626  frecabcl  6664  fopwdom  7130  phplem4dom  7157  phpm  7161  phplem4on  7163  fidifsnen  7166  diffisn  7191  diffifi  7192  en2eqpr  7208  fisseneq  7236  suplub2ti  7335  difinfsn  7434  ctmlemr  7442  ctm  7443  ctssdclemn0  7444  ctssdc  7447  nninfninc  7457  nninfisol  7467  enomnilem  7472  enmkvlem  7495  enwomnilem  7503  nninfwlpoimlemginf  7510  exmidontriimlem4  7574  exmidontriim  7575  cc3  7628  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  ltexnqq  7769  enq0tr  7795  addcmpblnq0  7804  mulcmpblnq0  7805  nnnq0lem1  7807  prssnqu  7841  prarloclemup  7856  nqprl  7912  nqpru  7913  mullocpr  7932  cauappcvgprlemladdfu  8015  cauappcvgprlemladdrl  8018  caucvgprlemm  8029  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgprlemlim  8042  caucvgprprlemml  8055  caucvgprprlemloc  8064  caucvgprprlemlim  8072  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  ltsrprg  8108  srpospr  8144  caucvgsrlemoffres  8161  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  axcaucvglemcau  8259  axsuploc  8392  cnegexlem3  8497  negeu  8511  add20  8796  rimul  8907  apreap  8909  cru  8924  apreim  8925  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  apti  8944  aptap  8972  mulap0  8976  prodgt0  9176  ltmul12a  9184  ledivdiv  9214  lediv12a  9218  supinfneg  9978  infsupneg  9979  qapne  10022  xaddf  10229  xaddval  10230  xleadd1a  10258  xleaddadd  10272  ixxss12  10291  ioodisj  10378  fznlem  10428  zsupcllemstep  10645  qtri3or  10658  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  addmodlteq  10818  seqf1og  10941  mulexpzap  10999  leexp1a  11014  expnbnd  11084  apexp1  11139  faclbnd  11162  hashxp  11250  sshashneg  11264  hashf1lem2  11269  zfz1iso  11276  swrdswrdlem  11459  cjap  11655  caucvgre  11730  cvg1nlemres  11734  resqrexlemglsq  11771  resqrexlemga  11772  sqrtsq  11793  ltabs  11836  abs3lem  11860  cau3lem  11863  maxleim  11954  rexico  11970  minmax  11979  xrmaxleim  11993  xrmaxiflemcl  11994  xrmaxiflemlub  11997  xrmaxiflemval  11999  xrmaxltsup  12007  xrmaxadd  12010  xrminmax  12014  xrbdtri  12025  climcau  12096  climrecvg1n  12097  sumeq2  12108  summodclem2  12132  divcnv  12247  prodeq2  12307  fprodsplitdc  12346  fprodconst  12370  dvdsle  12594  bitsfzo  12705  dvdsbnd  12716  bezoutlemmain  12758  bezoutlemzz  12762  bezoutlembi  12765  dfgcd3  12770  dvdsmulgcd  12785  nnmindc  12794  lcmcllem  12828  lcmgcdlem  12838  ncoprmgcdne1b  12850  isprm5  12903  pw2dvdslemn  12926  oddpwdclemxy  12930  pythagtriplem2  13028  pythagtrip  13045  pceu  13057  pc2dvds  13092  pcz  13094  pcadd  13102  pcfac  13112  exmidunben  13300  ctiunctlemfo  13313  unct  13316  sgrppropd  13711  sgrpidmndm  13716  mndpropd  13736  mhmeql  13782  isgrpinv  13842  dfgrp3mlem  13886  mhmmnd  13902  conjnmzb  14066  ghmcmn  14114  gzsumconst  14126  prdsval  14156  isrng  14216  issrg  14252  isring  14287  dvdsrmul1  14392  aprlring  14583  issubassa2  15018  tgrest  15253  cnpnei  15303  cnss1  15310  cncnp  15314  ismet2  15438  metequiv2  15580  metcnp  15596  metcnp2  15597  metcnpi3  15601  fsumcncntop  15651  elcncf2  15658  cncfmet  15676  suplociccreex  15708  dedekindicclemicc  15716  ivthinclemlr  15721  ivthinclemur  15723  cnplimclemr  15753  limccnpcntop  15759  limccoap  15762  dvmptfsum  15809  elply2  15819  plyrecj  15847  mersenne  16094  lgsval2lem  16112  lgsquad3  16186  usgr1eop  16469  usgr1vr  16472  pw1ndom3  17003  nninfalllem1  17025  nnnninfex  17039  sbthom  17045  apdiff  17071