Theorem simprrl 541

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

Assertion

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

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 491	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:  dn1dc  969  imain  5440  tfrlemisucaccv  6558  tfrexlem  6567  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  eroveu  6862  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  nqnq0pi  7758  addcmpblnq0  7763  mulcmpblnq0  7764  prarloclemcalc  7822  prarloc  7823  nqpru  7872  mullocpr  7891  distrlem4prl  7904  distrlem4pru  7905  ltprordil  7909  ltexprlemm  7920  ltexprlemopu  7923  ltexprlemupu  7924  ltexprlemru  7932  cauappcvgprlemopl  7966  cauappcvgprlem2  7980  caucvgprlemopl  7989  caucvgprlem2  8000  caucvgprprlemexbt  8026  caucvgprprlem2  8030  suplocexprlemloc  8041  suplocexprlemub  8043  suplocexprlemlub  8044  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  prsrlem1  8062  ltsrprg  8067  axmulcl  8186  ltmul1  8871  divdivdivap  8992  divmuleqap  8996  divsubdivap  9007  lt2mul2div  9158  ledivdiv  9169  lediv12a  9173  ssfzo12bi  10577  suprzcl2dc  10606  exbtwnz  10617  qbtwnre  10623  ioom  10627  seq3caopr  10864  seqcaoprg  10865  leexp2r  10962  hashunlem  11176  hashfibclem  11214  wrd2ind  11423  recvguniq  11688  rsqrmo  11720  fsum2dlemstep  12128  expcnvre  12197  fprod2dlemstep  12316  bezout  12715  qredeu  12802  pw2dvdseu  12873  oddpwdclemdvds  12875  pcqmul  13009  pcadd  13046  pockthg  13063  grprida  13621  issubmd  13708  ghmpreima  14004  unitgrp  14283  lmodprop2d  14545  lsspropdg  14628  neiint  15059  restbasg  15082  iscnp4  15132  cnpnei  15133  cnptopco  15136  blssps  15341  blss  15342  metequiv2  15410  xmetxpbl  15422  suplociccex  15539  dedekindicc  15547  limcimolemlt  15578  pellexlem3  15896  lgsquad2lem2  16004  2sqlem5  16041