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  3122  disjiun  4078  f1imass  5904  riota5f  5987  tfrexlem  6486  tfrcl  6516  nnsucuniel  6649  nntr2  6657  pw2f1odclem  7003  fopwdom  7005  fidceq  7039  fisbth  7053  fientri3  7085  unsnfidcex  7090  undifdc  7094  iunfidisj  7121  fiuni  7153  ordiso2  7210  nninfninc  7298  acfun  7397  2omotaplemap  7451  ccfunen  7458  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  addcmpblnq0  7638  mulcmpblnq0  7639  prml  7672  addlocpr  7731  prmuloc  7761  mullocpr  7766  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemloc  7802  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  aptiprleml  7834  ltmprr  7837  cauappcvgprlemopl  7841  cauappcvgprlemopu  7843  cauappcvgprlemloc  7847  caucvgprlemopl  7864  caucvgprlemopu  7866  caucvgprlemloc  7870  caucvgprprlemopu  7894  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  caucvgprprlemaddq  7903  suplocexprlemrl  7912  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  ltsrprg  7942  mulgt0sr  7973  caucvgsrlemgt1  7990  suplocsrlemb  8001  axmulcl  8061  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  cnegexlem1  8329  negeu  8345  add20  8629  apreap  8742  cru  8757  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  mulge0  8774  mulap0  8809  divdivdivap  8868  prodgt0  9007  ltmul12a  9015  lt2mul2div  9034  ledivdiv  9045  lediv12a  9049  qapne  9842  xleadd1a  10077  ixxss12  10110  elfz0ubfz0  10329  qtri3or  10468  exbtwnzlemstep  10475  exbtwnzlemex  10477  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  btwnzge0  10528  iseqf1olemqf1o  10736  mulexpzap  10809  leexp1a  10824  hashen  11014  fihashdom  11033  hashun  11035  swrdccatin1  11265  pfxccatin12lem3  11272  pfxccat3  11274  cjap  11425  cvg1nlemres  11504  rsqrmo  11546  abslt  11607  abs3lem  11630  cau3lem  11633  rexanre  11739  xrmaxltsup  11777  climcau  11866  sumeq2  11878  summodc  11902  fisumss  11911  fsum2d  11954  fsumabs  11984  fsumiun  11996  prodeq2  12076  prodmodclem2  12096  fprodcl2lem  12124  fprodap0  12140  fprod2d  12142  fprodrec  12148  fprodap0f  12155  fprodle  12159  eirrap  12297  divalglemeunn  12440  divalglemeuneg  12442  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlembi  12534  bezoutlemeu  12536  qredeu  12627  isprm5lem  12671  pw2dvdseu  12698  sqrt2irrap  12710  pythagtriplem2  12797  pythagtrip  12814  pclemub  12818  pcqmul  12834  pcexp  12840  pcneg  12856  pcprmpw2  12864  pcadd  12871  prmpwdvds  12886  4sqlem13m  12934  ennnfonelemg  12982  ennnfonelemrnh  12995  ctiunctlemfo  13018  nninfdclemf1  13031  imasival  13347  sgrppropd  13454  ismndd  13478  mndpropd  13481  mhmeql  13533  mhmmnd  13661  mulgfng  13669  issubg4m  13738  ssnmz  13756  conjnmzb  13825  rngpropd  13926  ringpropd  14009  dvdsrtr  14073  islmod  14263  mplsubgfilemcl  14671  restbasg  14850  cnpnei  14901  cnptoprest2  14922  cnpdis  14924  lmtopcnp  14932  txcnp  14953  ismet2  15036  blininf  15106  metss2lem  15179  xmettxlem  15191  xmettx  15192  metcnp  15194  metcnpi3  15199  addcncntoplem  15243  fsumcncntop  15249  mulc1cncf  15271  cncfco  15273  mulcncf  15290  dedekindeulemuub  15299  dedekindeu  15305  dedekindicclemuub  15308  ivthinclemloc  15323  ivthinc  15325  limcimo  15347  limccnp2cntop  15359  dveflem  15408  plyf  15419  plyco  15441  plycj  15443  dvply2g  15448  logbgcd1irrap  15652  perfectlem2  15682  lgsdilem  15714  lgsquad2lem2  15769  lgsquad3  15771  2sqlem5  15806  2sqlem9  15811  usgredg4  16021  fidcen  16379  2omap  16388  pw1map  16390  qdencn  16425  apdiff  16446