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  3079  disjiun  4025  f1imass  5818  riota5f  5899  tfrexlem  6389  tfrcl  6419  nnsucuniel  6550  nntr2  6558  pw2f1odclem  6892  fopwdom  6894  fidceq  6927  fisbth  6941  fientri3  6973  unsnfidcex  6978  undifdc  6982  iunfidisj  7007  fiuni  7039  ordiso2  7096  nninfninc  7184  acfun  7269  2omotaplemap  7319  ccfunen  7326  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  addcmpblnq0  7505  mulcmpblnq0  7506  prml  7539  addlocpr  7598  prmuloc  7628  mullocpr  7633  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  aptiprleml  7701  ltmprr  7704  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemloc  7714  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemloc  7737  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  suplocexprlemrl  7779  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  ltsrprg  7809  mulgt0sr  7840  caucvgsrlemgt1  7857  suplocsrlemb  7868  axmulcl  7928  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  cnegexlem1  8196  negeu  8212  add20  8495  apreap  8608  cru  8623  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  mulge0  8640  mulap0  8675  divdivdivap  8734  prodgt0  8873  ltmul12a  8881  lt2mul2div  8900  ledivdiv  8911  lediv12a  8915  qapne  9707  xleadd1a  9942  ixxss12  9975  elfz0ubfz0  10194  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  btwnzge0  10372  iseqf1olemqf1o  10580  mulexpzap  10653  leexp1a  10668  hashen  10858  fihashdom  10877  hashun  10879  cjap  11053  cvg1nlemres  11132  rsqrmo  11174  abslt  11235  abs3lem  11258  cau3lem  11261  rexanre  11367  xrmaxltsup  11404  climcau  11493  sumeq2  11505  summodc  11529  fisumss  11538  fsum2d  11581  fsumabs  11611  fsumiun  11623  prodeq2  11703  prodmodclem2  11723  fprodcl2lem  11751  fprodap0  11767  fprod2d  11769  fprodrec  11775  fprodap0f  11782  fprodle  11786  eirrap  11924  divalglemeunn  12065  divalglemeuneg  12067  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlembi  12145  bezoutlemeu  12147  qredeu  12238  isprm5lem  12282  pw2dvdseu  12309  sqrt2irrap  12321  pythagtriplem2  12407  pythagtrip  12424  pclemub  12428  pcqmul  12444  pcexp  12450  pcneg  12466  pcprmpw2  12474  pcadd  12481  prmpwdvds  12496  4sqlem13m  12544  ennnfonelemg  12563  ennnfonelemrnh  12576  ctiunctlemfo  12599  nninfdclemf1  12612  imasival  12892  sgrppropd  12999  ismndd  13021  mndpropd  13024  mhmeql  13067  mhmmnd  13189  mulgfng  13197  issubg4m  13266  ssnmz  13284  conjnmzb  13353  rngpropd  13454  ringpropd  13537  dvdsrtr  13600  islmod  13790  restbasg  14347  cnpnei  14398  cnptoprest2  14419  cnpdis  14421  lmtopcnp  14429  txcnp  14450  ismet2  14533  blininf  14603  metss2lem  14676  xmettxlem  14688  xmettx  14689  metcnp  14691  metcnpi3  14696  addcncntoplem  14740  fsumcncntop  14746  mulc1cncf  14768  cncfco  14770  mulcncf  14787  dedekindeulemuub  14796  dedekindeu  14802  dedekindicclemuub  14805  ivthinclemloc  14820  ivthinc  14822  limcimo  14844  limccnp2cntop  14856  dveflem  14905  plyf  14916  plyco  14937  plycj  14939  logbgcd1irrap  15143  lgsdilem  15184  lgsquad2lem2  15239  lgsquad3  15241  2sqlem5  15276  2sqlem9  15281  qdencn  15587  apdiff  15608