Theorem simplrl 541

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

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 493	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:  rmob  3145  disjiun  4123  f1imass  5974  riota5f  6059  tfrexlem  6599  tfrcl  6629  nnsucuniel  6762  nntr2  6770  pw2f1odclem  7128  fopwdom  7130  fidceq  7165  fisbth  7181  fidcen  7197  fientri3  7216  unsnfidcex  7221  undifdc  7225  iunfidisj  7254  fiuni  7306  2omap  7312  ordiso2  7369  nninfninc  7457  acfun  7557  2omotaplemap  7617  ccfunen  7624  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  addcmpblnq0  7804  mulcmpblnq0  7805  prml  7838  addlocpr  7897  prmuloc  7927  mullocpr  7932  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemloc  7968  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  aptiprleml  8000  ltmprr  8003  cauappcvgprlemopl  8007  cauappcvgprlemopu  8009  cauappcvgprlemloc  8013  caucvgprlemopl  8030  caucvgprlemopu  8032  caucvgprlemloc  8036  caucvgprprlemopu  8060  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  caucvgprprlemaddq  8069  suplocexprlemrl  8078  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemub  8084  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  ltsrprg  8108  mulgt0sr  8139  caucvgsrlemgt1  8156  suplocsrlemb  8167  axmulcl  8227  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  cnegexlem1  8495  negeu  8511  add20  8796  apreap  8909  cru  8924  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  mulge0  8941  mulap0  8976  divdivdivap  9037  prodgt0  9176  ltmul12a  9184  lt2mul2div  9203  ledivdiv  9214  lediv12a  9218  qapne  10022  xleadd1a  10258  ixxss12  10291  elfz0ubfz0  10515  qtri3or  10658  exbtwnzlemstep  10665  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  btwnzge0  10718  iseqf1olemqf1o  10926  mulexpzap  10999  leexp1a  11014  hashen  11206  fihashdom  11226  hashun  11228  hashf1lem2  11269  swrdccatin1  11480  pfxccatin12lem3  11487  pfxccat3  11489  cjap  11655  cvg1nlemres  11734  rsqrmo  11776  abslt  11837  abs3lem  11860  cau3lem  11863  rexanre  11969  xrmaxltsup  12007  climcau  12096  sumeq2  12108  summodc  12133  fisumss  12142  fsum2d  12185  fsumabs  12215  fsumiun  12227  prodeq2  12307  prodmodclem2  12327  fprodcl2lem  12355  fprodap0  12371  fprod2d  12373  fprodrec  12379  fprodap0f  12386  fprodle  12390  eirrap  12528  divalglemeunn  12671  divalglemeuneg  12673  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlembi  12765  bezoutlemeu  12767  qredeu  12858  isprm5lem  12902  pw2dvdseu  12929  sqrt2irrap  12941  pythagtriplem2  13028  pythagtrip  13045  pclemub  13049  pcqmul  13065  pcexp  13071  pcneg  13087  pcprmpw2  13095  pcadd  13102  prmpwdvds  13117  4sqlem13m  13165  ballotfilemsf1o  13240  ennnfonelemg  13277  ennnfonelemrnh  13290  ctiunctlemfo  13313  nninfdclemf1  13326  imasival  13610  sgrppropd  13711  ismndd  13733  mndpropd  13736  mhmeql  13782  mhmmnd  13902  mulgfng  13910  issubg4m  13979  ssnmz  13997  conjnmzb  14066  gsumvalfi  14135  rngpropd  14237  ringpropd  14326  dvdsrtr  14391  aprlring  14583  islmod  14610  assapropd  14997  mplsubgfilemcl  15073  restbasg  15252  cnpnei  15303  cnptoprest2  15324  cnpdis  15326  lmtopcnp  15334  txcnp  15355  ismet2  15438  blininf  15508  metss2lem  15581  xmettxlem  15593  xmettx  15594  metcnp  15596  metcnpi3  15601  addcncntoplem  15645  fsumcncntop  15651  mulc1cncf  15673  cncfco  15675  mulcncf  15692  dedekindeulemuub  15701  dedekindeu  15707  dedekindicclemuub  15710  ivthinclemloc  15725  ivthinc  15727  limcimo  15749  limccnp2cntop  15761  dveflem  15810  plyf  15821  plyco  15843  plycj  15845  dvply2g  15850  logbgcd1irrap  16055  perfectlem2  16097  lgsdilem  16129  lgsquad2lem2  16184  lgsquad3  16186  2sqlem5  16221  2sqlem9  16226  usgredg4  16439  usgr1eop  16469  usgr1vr  16472  subuhgr  16496  subumgr  16498  subusgr  16499  clwwlknonex2lem2  16662  pw1map  17008  qdencn  17046  apdiff  17071  qdiff  17072