Theorem simplrl 525

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 481	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3043  disjiun  3977  f1imass  5742  riota5f  5822  tfrexlem  6302  tfrcl  6332  nnsucuniel  6463  nntr2  6471  fopwdom  6802  fidceq  6835  fisbth  6849  fientri3  6880  unsnfidcex  6885  undifdc  6889  iunfidisj  6911  fiuni  6943  ordiso2  7000  acfun  7163  ccfunen  7205  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  addcmpblnq0  7384  mulcmpblnq0  7385  prml  7418  addlocpr  7477  prmuloc  7507  mullocpr  7512  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemloc  7548  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  aptiprleml  7580  ltmprr  7583  cauappcvgprlemopl  7587  cauappcvgprlemopu  7589  cauappcvgprlemloc  7593  caucvgprlemopl  7610  caucvgprlemopu  7612  caucvgprlemloc  7616  caucvgprprlemopu  7640  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  caucvgprprlemaddq  7649  suplocexprlemrl  7658  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  ltsrprg  7688  mulgt0sr  7719  caucvgsrlemgt1  7736  suplocsrlemb  7747  axmulcl  7807  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  cnegexlem1  8073  negeu  8089  add20  8372  apreap  8485  cru  8500  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  mulge0  8517  mulap0  8551  divdivdivap  8609  prodgt0  8747  ltmul12a  8755  lt2mul2div  8774  ledivdiv  8785  lediv12a  8789  qapne  9577  xleadd1a  9809  ixxss12  9842  elfz0ubfz0  10060  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2z  10190  btwnzge0  10235  iseqf1olemqf1o  10428  mulexpzap  10495  leexp1a  10510  hashen  10697  fihashdom  10716  hashun  10718  cjap  10848  cvg1nlemres  10927  rsqrmo  10969  abslt  11030  abs3lem  11053  cau3lem  11056  rexanre  11162  xrmaxltsup  11199  climcau  11288  sumeq2  11300  summodc  11324  fisumss  11333  fsum2d  11376  fsumabs  11406  fsumiun  11418  prodeq2  11498  prodmodclem2  11518  fprodcl2lem  11546  fprodap0  11562  fprod2d  11564  fprodrec  11570  fprodap0f  11577  fprodle  11581  eirrap  11718  divalglemeunn  11858  divalglemeuneg  11860  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlembi  11938  bezoutlemeu  11940  qredeu  12029  isprm5lem  12073  pw2dvdseu  12100  sqrt2irrap  12112  pythagtriplem2  12198  pythagtrip  12215  pclemub  12219  pcqmul  12235  pcexp  12241  pcneg  12256  pcprmpw2  12264  pcadd  12271  prmpwdvds  12285  ennnfonelemg  12336  ennnfonelemrnh  12349  ctiunctlemfo  12372  nninfdclemf1  12385  restbasg  12818  cnpnei  12869  cnptoprest2  12890  cnpdis  12892  lmtopcnp  12900  txcnp  12921  ismet2  13004  blininf  13074  metss2lem  13147  xmettxlem  13159  xmettx  13160  metcnp  13162  metcnpi3  13167  addcncntoplem  13201  fsumcncntop  13206  mulc1cncf  13226  cncfco  13228  mulcncf  13241  dedekindeulemuub  13245  dedekindeu  13251  dedekindicclemuub  13254  ivthinclemloc  13269  ivthinc  13271  limcimo  13284  limccnp2cntop  13296  dveflem  13337  logbgcd1irrap  13538  lgsdilem  13578  2sqlem5  13605  2sqlem9  13610  qdencn  13916  apdiff  13937