Theorem simpllr 534

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 488	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  542  f1o2ndf1  6286  tfrlem1  6366  tfr1onlemaccex  6406  tfrcllemaccex  6419  frecabcl  6457  fopwdom  6897  phplem4dom  6923  phpm  6926  phplem4on  6928  fidifsnen  6931  diffisn  6954  diffifi  6955  en2eqpr  6968  fisseneq  6995  suplub2ti  7067  difinfsn  7166  ctmlemr  7174  ctm  7175  ctssdclemn0  7176  ctssdc  7179  nninfninc  7189  nninfisol  7199  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  nninfwlpoimlemginf  7242  exmidontriimlem4  7291  exmidontriim  7292  cc3  7335  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  ltexnqq  7475  enq0tr  7501  addcmpblnq0  7510  mulcmpblnq0  7511  nnnq0lem1  7513  prssnqu  7547  prarloclemup  7562  nqprl  7618  nqpru  7619  mullocpr  7638  cauappcvgprlemladdfu  7721  cauappcvgprlemladdrl  7724  caucvgprlemm  7735  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlemlim  7748  caucvgprprlemml  7761  caucvgprprlemloc  7770  caucvgprprlemlim  7778  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  ltsrprg  7814  srpospr  7850  caucvgsrlemoffres  7867  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axcaucvglemcau  7965  axsuploc  8099  cnegexlem3  8203  negeu  8217  add20  8501  rimul  8612  apreap  8614  cru  8629  apreim  8630  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  apti  8649  aptap  8677  mulap0  8681  prodgt0  8879  ltmul12a  8887  ledivdiv  8917  lediv12a  8921  supinfneg  9669  infsupneg  9670  qapne  9713  xaddf  9919  xaddval  9920  xleadd1a  9948  xleaddadd  9962  ixxss12  9981  ioodisj  10068  fznlem  10116  zsupcllemstep  10319  qtri3or  10330  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  addmodlteq  10490  seqf1og  10613  mulexpzap  10671  leexp1a  10686  expnbnd  10755  apexp1  10810  faclbnd  10833  hashxp  10918  zfz1iso  10933  cjap  11071  caucvgre  11146  cvg1nlemres  11150  resqrexlemglsq  11187  resqrexlemga  11188  sqrtsq  11209  ltabs  11252  abs3lem  11276  cau3lem  11279  maxleim  11370  rexico  11386  minmax  11395  xrmaxleim  11409  xrmaxiflemcl  11410  xrmaxiflemlub  11413  xrmaxiflemval  11415  xrmaxltsup  11423  xrmaxadd  11426  xrminmax  11430  xrbdtri  11441  climcau  11512  climrecvg1n  11513  sumeq2  11524  summodclem2  11547  divcnv  11662  prodeq2  11722  fprodsplitdc  11761  fprodconst  11785  dvdsle  12009  bitsfzo  12119  dvdsbnd  12123  bezoutlemmain  12165  bezoutlemzz  12169  bezoutlembi  12172  dfgcd3  12177  dvdsmulgcd  12192  nnmindc  12201  lcmcllem  12235  lcmgcdlem  12245  ncoprmgcdne1b  12257  isprm5  12310  pw2dvdslemn  12333  oddpwdclemxy  12337  pythagtriplem2  12435  pythagtrip  12452  pceu  12464  pc2dvds  12499  pcz  12501  pcadd  12509  pcfac  12519  exmidunben  12643  ctiunctlemfo  12656  unct  12659  sgrppropd  13056  sgrpidmndm  13061  mndpropd  13081  mhmeql  13124  isgrpinv  13186  dfgrp3mlem  13230  mhmmnd  13246  conjnmzb  13410  ghmcmn  13457  gsumfzconst  13471  isrng  13490  issrg  13521  isring  13556  reldvdsrsrg  13648  dvdsrmul1  13658  tgrest  14405  cnpnei  14455  cnss1  14462  cncnp  14466  ismet2  14590  metequiv2  14732  metcnp  14748  metcnp2  14749  metcnpi3  14753  fsumcncntop  14803  elcncf2  14810  cncfmet  14828  suplociccreex  14860  dedekindicclemicc  14868  ivthinclemlr  14873  ivthinclemur  14875  cnplimclemr  14905  limccnpcntop  14911  limccoap  14914  dvmptfsum  14961  elply2  14971  plyrecj  14999  mersenne  15233  lgsval2lem  15251  lgsquad3  15325  nninfalllem1  15652  sbthom  15670  apdiff  15692