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  3055  disjiun  3996  f1imass  5770  riota5f  5850  tfrexlem  6330  tfrcl  6360  nnsucuniel  6491  nntr2  6499  fopwdom  6831  fidceq  6864  fisbth  6878  fientri3  6909  unsnfidcex  6914  undifdc  6918  iunfidisj  6940  fiuni  6972  ordiso2  7029  acfun  7201  2omotaplemap  7251  ccfunen  7258  addcmpblnq  7361  mulcmpblnq  7362  ordpipqqs  7368  addcmpblnq0  7437  mulcmpblnq0  7438  prml  7471  addlocpr  7530  prmuloc  7560  mullocpr  7565  ltexprlemopl  7595  ltexprlemopu  7597  ltexprlemloc  7601  ltexprlemrl  7604  ltexprlemru  7606  addcanprleml  7608  addcanprlemu  7609  aptiprleml  7633  ltmprr  7636  cauappcvgprlemopl  7640  cauappcvgprlemopu  7642  cauappcvgprlemloc  7646  caucvgprlemopl  7663  caucvgprlemopu  7665  caucvgprlemloc  7669  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemexbt  7700  caucvgprprlemaddq  7702  suplocexprlemrl  7711  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  ltsrprg  7741  mulgt0sr  7772  caucvgsrlemgt1  7789  suplocsrlemb  7800  axmulcl  7860  axcaucvglemres  7893  axpre-suploclemres  7895  axpre-suploc  7896  cnegexlem1  8126  negeu  8142  add20  8425  apreap  8538  cru  8553  apsym  8557  apcotr  8558  apadd1  8559  apneg  8562  mulext1  8563  mulge0  8570  mulap0  8605  divdivdivap  8664  prodgt0  8803  ltmul12a  8811  lt2mul2div  8830  ledivdiv  8841  lediv12a  8845  qapne  9633  xleadd1a  9867  ixxss12  9900  elfz0ubfz0  10118  qtri3or  10236  exbtwnzlemstep  10241  exbtwnzlemex  10243  exbtwnz  10244  rebtwn2zlemstep  10246  rebtwn2z  10248  btwnzge0  10293  iseqf1olemqf1o  10486  mulexpzap  10553  leexp1a  10568  hashen  10755  fihashdom  10774  hashun  10776  cjap  10906  cvg1nlemres  10985  rsqrmo  11027  abslt  11088  abs3lem  11111  cau3lem  11114  rexanre  11220  xrmaxltsup  11257  climcau  11346  sumeq2  11358  summodc  11382  fisumss  11391  fsum2d  11434  fsumabs  11464  fsumiun  11476  prodeq2  11556  prodmodclem2  11576  fprodcl2lem  11604  fprodap0  11620  fprod2d  11622  fprodrec  11628  fprodap0f  11635  fprodle  11639  eirrap  11776  divalglemeunn  11916  divalglemeuneg  11918  bezoutlemnewy  11987  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlembi  11996  bezoutlemeu  11998  qredeu  12087  isprm5lem  12131  pw2dvdseu  12158  sqrt2irrap  12170  pythagtriplem2  12256  pythagtrip  12273  pclemub  12277  pcqmul  12293  pcexp  12299  pcneg  12314  pcprmpw2  12322  pcadd  12329  prmpwdvds  12343  ennnfonelemg  12394  ennnfonelemrnh  12407  ctiunctlemfo  12430  nninfdclemf1  12443  ismndd  12768  mndpropd  12771  mhmeql  12804  mhmmnd  12908  mulgfng  12915  issubg4m  12979  ringpropd  13117  dvdsrtr  13169  restbasg  13450  cnpnei  13501  cnptoprest2  13522  cnpdis  13524  lmtopcnp  13532  txcnp  13553  ismet2  13636  blininf  13706  metss2lem  13779  xmettxlem  13791  xmettx  13792  metcnp  13794  metcnpi3  13799  addcncntoplem  13833  fsumcncntop  13838  mulc1cncf  13858  cncfco  13860  mulcncf  13873  dedekindeulemuub  13877  dedekindeu  13883  dedekindicclemuub  13886  ivthinclemloc  13901  ivthinc  13903  limcimo  13916  limccnp2cntop  13928  dveflem  13969  logbgcd1irrap  14170  lgsdilem  14210  2sqlem5  14237  2sqlem9  14242  qdencn  14546  apdiff  14567