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  3057  disjiun  4000  f1imass  5777  riota5f  5857  tfrexlem  6337  tfrcl  6367  nnsucuniel  6498  nntr2  6506  fopwdom  6838  fidceq  6871  fisbth  6885  fientri3  6916  unsnfidcex  6921  undifdc  6925  iunfidisj  6947  fiuni  6979  ordiso2  7036  acfun  7208  2omotaplemap  7258  ccfunen  7265  addcmpblnq  7368  mulcmpblnq  7369  ordpipqqs  7375  addcmpblnq0  7444  mulcmpblnq0  7445  prml  7478  addlocpr  7537  prmuloc  7567  mullocpr  7572  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  aptiprleml  7640  ltmprr  7643  cauappcvgprlemopl  7647  cauappcvgprlemopu  7649  cauappcvgprlemloc  7653  caucvgprlemopl  7670  caucvgprlemopu  7672  caucvgprlemloc  7676  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  caucvgprprlemaddq  7709  suplocexprlemrl  7718  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  addcmpblnr  7740  mulcmpblnrlemg  7741  mulcmpblnr  7742  ltsrprg  7748  mulgt0sr  7779  caucvgsrlemgt1  7796  suplocsrlemb  7807  axmulcl  7867  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  cnegexlem1  8134  negeu  8150  add20  8433  apreap  8546  cru  8561  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  mulge0  8578  mulap0  8613  divdivdivap  8672  prodgt0  8811  ltmul12a  8819  lt2mul2div  8838  ledivdiv  8849  lediv12a  8853  qapne  9641  xleadd1a  9875  ixxss12  9908  elfz0ubfz0  10127  qtri3or  10245  exbtwnzlemstep  10250  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  btwnzge0  10302  iseqf1olemqf1o  10495  mulexpzap  10562  leexp1a  10577  hashen  10766  fihashdom  10785  hashun  10787  cjap  10917  cvg1nlemres  10996  rsqrmo  11038  abslt  11099  abs3lem  11122  cau3lem  11125  rexanre  11231  xrmaxltsup  11268  climcau  11357  sumeq2  11369  summodc  11393  fisumss  11402  fsum2d  11445  fsumabs  11475  fsumiun  11487  prodeq2  11567  prodmodclem2  11587  fprodcl2lem  11615  fprodap0  11631  fprod2d  11633  fprodrec  11639  fprodap0f  11646  fprodle  11650  eirrap  11787  divalglemeunn  11928  divalglemeuneg  11930  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlembi  12008  bezoutlemeu  12010  qredeu  12099  isprm5lem  12143  pw2dvdseu  12170  sqrt2irrap  12182  pythagtriplem2  12268  pythagtrip  12285  pclemub  12289  pcqmul  12305  pcexp  12311  pcneg  12326  pcprmpw2  12334  pcadd  12341  prmpwdvds  12355  ennnfonelemg  12406  ennnfonelemrnh  12419  ctiunctlemfo  12442  nninfdclemf1  12455  imasival  12732  ismndd  12843  mndpropd  12846  mhmeql  12881  mhmmnd  12985  mulgfng  12992  issubg4m  13058  ssnmz  13076  ringpropd  13222  dvdsrtr  13275  islmod  13386  restbasg  13707  cnpnei  13758  cnptoprest2  13779  cnpdis  13781  lmtopcnp  13789  txcnp  13810  ismet2  13893  blininf  13963  metss2lem  14036  xmettxlem  14048  xmettx  14049  metcnp  14051  metcnpi3  14056  addcncntoplem  14090  fsumcncntop  14095  mulc1cncf  14115  cncfco  14117  mulcncf  14130  dedekindeulemuub  14134  dedekindeu  14140  dedekindicclemuub  14143  ivthinclemloc  14158  ivthinc  14160  limcimo  14173  limccnp2cntop  14185  dveflem  14226  logbgcd1irrap  14427  lgsdilem  14467  2sqlem5  14505  2sqlem9  14510  qdencn  14814  apdiff  14835