Theorem simplrl 535

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 489	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  3082  disjiun  4028  f1imass  5821  riota5f  5902  tfrexlem  6392  tfrcl  6422  nnsucuniel  6553  nntr2  6561  pw2f1odclem  6895  fopwdom  6897  fidceq  6930  fisbth  6944  fientri3  6976  unsnfidcex  6981  undifdc  6985  iunfidisj  7012  fiuni  7044  ordiso2  7101  nninfninc  7189  acfun  7274  2omotaplemap  7324  ccfunen  7331  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  addcmpblnq0  7510  mulcmpblnq0  7511  prml  7544  addlocpr  7603  prmuloc  7633  mullocpr  7638  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  aptiprleml  7706  ltmprr  7709  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemloc  7719  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemloc  7742  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  suplocexprlemrl  7784  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  ltsrprg  7814  mulgt0sr  7845  caucvgsrlemgt1  7862  suplocsrlemb  7873  axmulcl  7933  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  cnegexlem1  8201  negeu  8217  add20  8501  apreap  8614  cru  8629  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  mulge0  8646  mulap0  8681  divdivdivap  8740  prodgt0  8879  ltmul12a  8887  lt2mul2div  8906  ledivdiv  8917  lediv12a  8921  qapne  9713  xleadd1a  9948  ixxss12  9981  elfz0ubfz0  10200  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  btwnzge0  10390  iseqf1olemqf1o  10598  mulexpzap  10671  leexp1a  10686  hashen  10876  fihashdom  10895  hashun  10897  cjap  11071  cvg1nlemres  11150  rsqrmo  11192  abslt  11253  abs3lem  11276  cau3lem  11279  rexanre  11385  xrmaxltsup  11423  climcau  11512  sumeq2  11524  summodc  11548  fisumss  11557  fsum2d  11600  fsumabs  11630  fsumiun  11642  prodeq2  11722  prodmodclem2  11742  fprodcl2lem  11770  fprodap0  11786  fprod2d  11788  fprodrec  11794  fprodap0f  11801  fprodle  11805  eirrap  11943  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlembi  12172  bezoutlemeu  12174  qredeu  12265  isprm5lem  12309  pw2dvdseu  12336  sqrt2irrap  12348  pythagtriplem2  12435  pythagtrip  12452  pclemub  12456  pcqmul  12472  pcexp  12478  pcneg  12494  pcprmpw2  12502  pcadd  12509  prmpwdvds  12524  4sqlem13m  12572  ennnfonelemg  12620  ennnfonelemrnh  12633  ctiunctlemfo  12656  nninfdclemf1  12669  imasival  12949  sgrppropd  13056  ismndd  13078  mndpropd  13081  mhmeql  13124  mhmmnd  13246  mulgfng  13254  issubg4m  13323  ssnmz  13341  conjnmzb  13410  rngpropd  13511  ringpropd  13594  dvdsrtr  13657  islmod  13847  restbasg  14404  cnpnei  14455  cnptoprest2  14476  cnpdis  14478  lmtopcnp  14486  txcnp  14507  ismet2  14590  blininf  14660  metss2lem  14733  xmettxlem  14745  xmettx  14746  metcnp  14748  metcnpi3  14753  addcncntoplem  14797  fsumcncntop  14803  mulc1cncf  14825  cncfco  14827  mulcncf  14844  dedekindeulemuub  14853  dedekindeu  14859  dedekindicclemuub  14862  ivthinclemloc  14877  ivthinc  14879  limcimo  14901  limccnp2cntop  14913  dveflem  14962  plyf  14973  plyco  14995  plycj  14997  dvply2g  15002  logbgcd1irrap  15206  perfectlem2  15236  lgsdilem  15268  lgsquad2lem2  15323  lgsquad3  15325  2sqlem5  15360  2sqlem9  15365  qdencn  15671  apdiff  15692