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  5907  riota5f  5990  tfrexlem  6491  tfrcl  6521  nnsucuniel  6654  nntr2  6662  pw2f1odclem  7008  fopwdom  7010  fidceq  7044  fisbth  7058  fidcen  7074  fientri3  7093  unsnfidcex  7098  undifdc  7102  iunfidisj  7129  fiuni  7161  ordiso2  7218  nninfninc  7306  acfun  7405  2omotaplemap  7459  ccfunen  7466  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  addcmpblnq0  7646  mulcmpblnq0  7647  prml  7680  addlocpr  7739  prmuloc  7769  mullocpr  7774  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemloc  7810  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  aptiprleml  7842  ltmprr  7845  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlemloc  7855  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlemloc  7878  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlemaddq  7911  suplocexprlemrl  7920  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  ltsrprg  7950  mulgt0sr  7981  caucvgsrlemgt1  7998  suplocsrlemb  8009  axmulcl  8069  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  cnegexlem1  8337  negeu  8353  add20  8637  apreap  8750  cru  8765  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  mulge0  8782  mulap0  8817  divdivdivap  8876  prodgt0  9015  ltmul12a  9023  lt2mul2div  9042  ledivdiv  9053  lediv12a  9057  qapne  9851  xleadd1a  10086  ixxss12  10119  elfz0ubfz0  10338  qtri3or  10477  exbtwnzlemstep  10484  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  btwnzge0  10537  iseqf1olemqf1o  10745  mulexpzap  10818  leexp1a  10833  hashen  11023  fihashdom  11042  hashun  11044  swrdccatin1  11278  pfxccatin12lem3  11285  pfxccat3  11287  cjap  11438  cvg1nlemres  11517  rsqrmo  11559  abslt  11620  abs3lem  11643  cau3lem  11646  rexanre  11752  xrmaxltsup  11790  climcau  11879  sumeq2  11891  summodc  11915  fisumss  11924  fsum2d  11967  fsumabs  11997  fsumiun  12009  prodeq2  12089  prodmodclem2  12109  fprodcl2lem  12137  fprodap0  12153  fprod2d  12155  fprodrec  12161  fprodap0f  12168  fprodle  12172  eirrap  12310  divalglemeunn  12453  divalglemeuneg  12455  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlembi  12547  bezoutlemeu  12549  qredeu  12640  isprm5lem  12684  pw2dvdseu  12711  sqrt2irrap  12723  pythagtriplem2  12810  pythagtrip  12827  pclemub  12831  pcqmul  12847  pcexp  12853  pcneg  12869  pcprmpw2  12877  pcadd  12884  prmpwdvds  12899  4sqlem13m  12947  ennnfonelemg  12995  ennnfonelemrnh  13008  ctiunctlemfo  13031  nninfdclemf1  13044  imasival  13360  sgrppropd  13467  ismndd  13491  mndpropd  13494  mhmeql  13546  mhmmnd  13674  mulgfng  13682  issubg4m  13751  ssnmz  13769  conjnmzb  13838  rngpropd  13939  ringpropd  14022  dvdsrtr  14086  islmod  14276  mplsubgfilemcl  14684  restbasg  14863  cnpnei  14914  cnptoprest2  14935  cnpdis  14937  lmtopcnp  14945  txcnp  14966  ismet2  15049  blininf  15119  metss2lem  15192  xmettxlem  15204  xmettx  15205  metcnp  15207  metcnpi3  15212  addcncntoplem  15256  fsumcncntop  15262  mulc1cncf  15284  cncfco  15286  mulcncf  15303  dedekindeulemuub  15312  dedekindeu  15318  dedekindicclemuub  15321  ivthinclemloc  15336  ivthinc  15338  limcimo  15360  limccnp2cntop  15372  dveflem  15421  plyf  15432  plyco  15454  plycj  15456  dvply2g  15461  logbgcd1irrap  15665  perfectlem2  15695  lgsdilem  15727  lgsquad2lem2  15782  lgsquad3  15784  2sqlem5  15819  2sqlem9  15824  usgredg4  16034  usgr1eop  16064  usgr1vr  16067  2omap  16472  pw1map  16474  qdencn  16509  apdiff  16530